Theorem fisub 10541

Description: If a set has the finite intersection property, its subsets have also this property.

Hypotheses

Ref	Expression
fisub.1	⊢ B = {z∣∃y(y ⊆ A ⋀ ∃u ∈ ω y ≈ u ⋀ z = ∩y)}
fisub.2	⊢ D = {z∣∃y(y ⊆ C ⋀ ∃u ∈ ω y ≈ u ⋀ z = ∩y)}

Assertion

Ref	Expression
fisub	⊢ (C ⊆ A → (¬ ∅ ∈ B → ¬ ∅ ∈ D))

Distinct variable groups:   y,A,z   y,B   y,C,z   z,u

Proof of Theorem fisub

Step	Hyp	Ref	Expression
1		sstr 2070	. . . . . . . . 9 ⊢ ((y ⊆ C ⋀ C ⊆ A) → y ⊆ A)
2		0ex 2708	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
3		eqeq1 1480	. . . . . . . . . . . . . . 15 ⊢ (z = ∅ → (z = ∩y ↔ ∅ = ∩y))
4	3	3anbi3d 898	. . . . . . . . . . . . . 14 ⊢ (z = ∅ → ((y ⊆ A ⋀ ∃u ∈ ω y ≈ u ⋀ z = ∩y) ↔ (y ⊆ A ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y)))
5	4	exbidv 1279	. . . . . . . . . . . . 13 ⊢ (z = ∅ → (∃y(y ⊆ A ⋀ ∃u ∈ ω y ≈ u ⋀ z = ∩y) ↔ ∃y(y ⊆ A ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y)))
6		fisub.1	. . . . . . . . . . . . 13 ⊢ B = {z∣∃y(y ⊆ A ⋀ ∃u ∈ ω y ≈ u ⋀ z = ∩y)}
7	2, 5, 6	elab2 1899	. . . . . . . . . . . 12 ⊢ (∅ ∈ B ↔ ∃y(y ⊆ A ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y))
8	7	biimpr 152	. . . . . . . . . . 11 ⊢ (∃y(y ⊆ A ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y) → ∅ ∈ B)
9	8	19.23bi 1064	. . . . . . . . . 10 ⊢ ((y ⊆ A ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y) → ∅ ∈ B)
10	9	3exp 831	. . . . . . . . 9 ⊢ (y ⊆ A → (∃u ∈ ω y ≈ u → (∅ = ∩y → ∅ ∈ B)))
11	1, 10	syl 10	. . . . . . . 8 ⊢ ((y ⊆ C ⋀ C ⊆ A) → (∃u ∈ ω y ≈ u → (∅ = ∩y → ∅ ∈ B)))
12	11	expcom 374	. . . . . . 7 ⊢ (C ⊆ A → (y ⊆ C → (∃u ∈ ω y ≈ u → (∅ = ∩y → ∅ ∈ B))))
13	12	com4l 39	. . . . . 6 ⊢ (y ⊆ C → (∃u ∈ ω y ≈ u → (∅ = ∩y → (C ⊆ A → ∅ ∈ B))))
14	13	3imp 826	. . . . 5 ⊢ ((y ⊆ C ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y) → (C ⊆ A → ∅ ∈ B))
15	14	19.23aiv 1295	. . . 4 ⊢ (∃y(y ⊆ C ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y) → (C ⊆ A → ∅ ∈ B))
16	15	com12 11	. . 3 ⊢ (C ⊆ A → (∃y(y ⊆ C ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y) → ∅ ∈ B))
17	3	3anbi3d 898	. . . . 5 ⊢ (z = ∅ → ((y ⊆ C ⋀ ∃u ∈ ω y ≈ u ⋀ z = ∩y) ↔ (y ⊆ C ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y)))
18	17	exbidv 1279	. . . 4 ⊢ (z = ∅ → (∃y(y ⊆ C ⋀ ∃u ∈ ω y ≈ u ⋀ z = ∩y) ↔ ∃y(y ⊆ C ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y)))
19		fisub.2	. . . 4 ⊢ D = {z∣∃y(y ⊆ C ⋀ ∃u ∈ ω y ≈ u ⋀ z = ∩y)}
20	2, 18, 19	elab2 1899	. . 3 ⊢ (∅ ∈ D ↔ ∃y(y ⊆ C ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y))
21	16, 20	syl5ib 206	. 2 ⊢ (C ⊆ A → (∅ ∈ D → ∅ ∈ B))
22	21	con3d 95	1 ⊢ (C ⊆ A → (¬ ∅ ∈ B → ¬ ∅ ∈ D))

Syntax hints:  ¬ wn 2   → wi 3   ⋀ wa 223   ⋀ w3a 774   = wceq 955   ∈ wcel 957  ∃wex 979  {cab 1463  ∃wrex 1645   ⊆ wss 2045  ∅c0 2278  ∩cint 2530   class class class wbr 2616  ωcom 3128   ≈ cen 4361

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-nul 2707

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-v 1810  df-dif 2047  df-in 2049  df-ss 2051  df-nul 2279

Copyright terms: Public domain