Metamath Proof Explorer

Theorem acsfn

Description: Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion acsfn ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin → a ∈ 𝒫 X | T ⊆ a → K ∈ a ∈ ACS ⁡ X

Proof

Step Hyp Ref Expression
1 funmpt ⊢ Fun ⁡ b ∈ 𝒫 X ⟼ if b = T K ∅
2 funiunfv ⊢ Fun ⁡ b ∈ 𝒫 X ⟼ if b = T K ∅ → ⋃ c ∈ 𝒫 a ∩ Fin b ∈ 𝒫 X ⟼ if b = T K ∅ ⁡ c = ⋃ b ∈ 𝒫 X ⟼ if b = T K ∅ 𝒫 a ∩ Fin
3 1 2 mp1i ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → ⋃ c ∈ 𝒫 a ∩ Fin b ∈ 𝒫 X ⟼ if b = T K ∅ ⁡ c = ⋃ b ∈ 𝒫 X ⟼ if b = T K ∅ 𝒫 a ∩ Fin
4 elinel1 ⊢ c ∈ 𝒫 a ∩ Fin → c ∈ 𝒫 a
5 4 elpwid ⊢ c ∈ 𝒫 a ∩ Fin → c ⊆ a
6 elpwi ⊢ a ∈ 𝒫 X → a ⊆ X
7 5 6 sylan9ssr ⊢ a ∈ 𝒫 X ∧ c ∈ 𝒫 a ∩ Fin → c ⊆ X
8 velpw ⊢ c ∈ 𝒫 X ↔ c ⊆ X
9 7 8 sylibr ⊢ a ∈ 𝒫 X ∧ c ∈ 𝒫 a ∩ Fin → c ∈ 𝒫 X
10 9 adantll ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X ∧ c ∈ 𝒫 a ∩ Fin → c ∈ 𝒫 X
11 eqeq1 ⊢ b = c → b = T ↔ c = T
12 11 ifbid ⊢ b = c → if b = T K ∅ = if c = T K ∅
13 eqid ⊢ b ∈ 𝒫 X ⟼ if b = T K ∅ = b ∈ 𝒫 X ⟼ if b = T K ∅
14 snex ⊢ K ∈ V
15 0ex ⊢ ∅ ∈ V
16 14 15 ifex ⊢ if c = T K ∅ ∈ V
17 12 13 16 fvmpt ⊢ c ∈ 𝒫 X → b ∈ 𝒫 X ⟼ if b = T K ∅ ⁡ c = if c = T K ∅
18 10 17 syl ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X ∧ c ∈ 𝒫 a ∩ Fin → b ∈ 𝒫 X ⟼ if b = T K ∅ ⁡ c = if c = T K ∅
19 18 iuneq2dv ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → ⋃ c ∈ 𝒫 a ∩ Fin b ∈ 𝒫 X ⟼ if b = T K ∅ ⁡ c = ⋃ c ∈ 𝒫 a ∩ Fin if c = T K ∅
20 3 19 eqtr3d ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → ⋃ b ∈ 𝒫 X ⟼ if b = T K ∅ 𝒫 a ∩ Fin = ⋃ c ∈ 𝒫 a ∩ Fin if c = T K ∅
21 20 sseq1d ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → ⋃ b ∈ 𝒫 X ⟼ if b = T K ∅ 𝒫 a ∩ Fin ⊆ a ↔ ⋃ c ∈ 𝒫 a ∩ Fin if c = T K ∅ ⊆ a
22 iunss ⊢ ⋃ c ∈ 𝒫 a ∩ Fin if c = T K ∅ ⊆ a ↔ ∀ c ∈ 𝒫 a ∩ Fin if c = T K ∅ ⊆ a
23 sseq1 ⊢ K = if c = T K ∅ → K ⊆ a ↔ if c = T K ∅ ⊆ a
24 23 bibi1d ⊢ K = if c = T K ∅ → K ⊆ a ↔ c = T → K ∈ a ↔ if c = T K ∅ ⊆ a ↔ c = T → K ∈ a
25 sseq1 ⊢ ∅ = if c = T K ∅ → ∅ ⊆ a ↔ if c = T K ∅ ⊆ a
26 25 bibi1d ⊢ ∅ = if c = T K ∅ → ∅ ⊆ a ↔ c = T → K ∈ a ↔ if c = T K ∅ ⊆ a ↔ c = T → K ∈ a
27 snssg ⊢ K ∈ X → K ∈ a ↔ K ⊆ a
28 27 adantr ⊢ K ∈ X ∧ c = T → K ∈ a ↔ K ⊆ a
29 biimt ⊢ c = T → K ∈ a ↔ c = T → K ∈ a
30 29 adantl ⊢ K ∈ X ∧ c = T → K ∈ a ↔ c = T → K ∈ a
31 28 30 bitr3d ⊢ K ∈ X ∧ c = T → K ⊆ a ↔ c = T → K ∈ a
32 0ss ⊢ ∅ ⊆ a
33 32 a1i ⊢ ¬ c = T → ∅ ⊆ a
34 pm2.21 ⊢ ¬ c = T → c = T → K ∈ a
35 33 34 2thd ⊢ ¬ c = T → ∅ ⊆ a ↔ c = T → K ∈ a
36 35 adantl ⊢ K ∈ X ∧ ¬ c = T → ∅ ⊆ a ↔ c = T → K ∈ a
37 24 26 31 36 ifbothda ⊢ K ∈ X → if c = T K ∅ ⊆ a ↔ c = T → K ∈ a
38 37 ralbidv ⊢ K ∈ X → ∀ c ∈ 𝒫 a ∩ Fin if c = T K ∅ ⊆ a ↔ ∀ c ∈ 𝒫 a ∩ Fin c = T → K ∈ a
39 38 ad3antlr ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → ∀ c ∈ 𝒫 a ∩ Fin if c = T K ∅ ⊆ a ↔ ∀ c ∈ 𝒫 a ∩ Fin c = T → K ∈ a
40 22 39 bitrid ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → ⋃ c ∈ 𝒫 a ∩ Fin if c = T K ∅ ⊆ a ↔ ∀ c ∈ 𝒫 a ∩ Fin c = T → K ∈ a
41 inss1 ⊢ 𝒫 a ∩ Fin ⊆ 𝒫 a
42 6 sspwd ⊢ a ∈ 𝒫 X → 𝒫 a ⊆ 𝒫 X
43 41 42 sstrid ⊢ a ∈ 𝒫 X → 𝒫 a ∩ Fin ⊆ 𝒫 X
44 43 adantl ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → 𝒫 a ∩ Fin ⊆ 𝒫 X
45 ralss ⊢ 𝒫 a ∩ Fin ⊆ 𝒫 X → ∀ c ∈ 𝒫 a ∩ Fin c = T → K ∈ a ↔ ∀ c ∈ 𝒫 X c ∈ 𝒫 a ∩ Fin → c = T → K ∈ a
46 44 45 syl ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → ∀ c ∈ 𝒫 a ∩ Fin c = T → K ∈ a ↔ ∀ c ∈ 𝒫 X c ∈ 𝒫 a ∩ Fin → c = T → K ∈ a
47 bi2.04 ⊢ c ∈ 𝒫 a ∩ Fin → c = T → K ∈ a ↔ c = T → c ∈ 𝒫 a ∩ Fin → K ∈ a
48 47 ralbii ⊢ ∀ c ∈ 𝒫 X c ∈ 𝒫 a ∩ Fin → c = T → K ∈ a ↔ ∀ c ∈ 𝒫 X c = T → c ∈ 𝒫 a ∩ Fin → K ∈ a
49 elpwg ⊢ T ∈ Fin → T ∈ 𝒫 X ↔ T ⊆ X
50 49 biimparc ⊢ T ⊆ X ∧ T ∈ Fin → T ∈ 𝒫 X
51 50 ad2antlr ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → T ∈ 𝒫 X
52 eleq1 ⊢ c = T → c ∈ 𝒫 a ∩ Fin ↔ T ∈ 𝒫 a ∩ Fin
53 52 imbi1d ⊢ c = T → c ∈ 𝒫 a ∩ Fin → K ∈ a ↔ T ∈ 𝒫 a ∩ Fin → K ∈ a
54 53 ceqsralv ⊢ T ∈ 𝒫 X → ∀ c ∈ 𝒫 X c = T → c ∈ 𝒫 a ∩ Fin → K ∈ a ↔ T ∈ 𝒫 a ∩ Fin → K ∈ a
55 51 54 syl ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → ∀ c ∈ 𝒫 X c = T → c ∈ 𝒫 a ∩ Fin → K ∈ a ↔ T ∈ 𝒫 a ∩ Fin → K ∈ a
56 48 55 bitrid ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → ∀ c ∈ 𝒫 X c ∈ 𝒫 a ∩ Fin → c = T → K ∈ a ↔ T ∈ 𝒫 a ∩ Fin → K ∈ a
57 simplrr ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → T ∈ Fin
58 57 biantrud ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → T ∈ 𝒫 a ↔ T ∈ 𝒫 a ∧ T ∈ Fin
59 elin ⊢ T ∈ 𝒫 a ∩ Fin ↔ T ∈ 𝒫 a ∧ T ∈ Fin
60 58 59 bitr4di ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → T ∈ 𝒫 a ↔ T ∈ 𝒫 a ∩ Fin
61 vex ⊢ a ∈ V
62 61 elpw2 ⊢ T ∈ 𝒫 a ↔ T ⊆ a
63 60 62 bitr3di ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → T ∈ 𝒫 a ∩ Fin ↔ T ⊆ a
64 63 imbi1d ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → T ∈ 𝒫 a ∩ Fin → K ∈ a ↔ T ⊆ a → K ∈ a
65 46 56 64 3bitrd ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → ∀ c ∈ 𝒫 a ∩ Fin c = T → K ∈ a ↔ T ⊆ a → K ∈ a
66 21 40 65 3bitrrd ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ a ∈ 𝒫 X → T ⊆ a → K ∈ a ↔ ⋃ b ∈ 𝒫 X ⟼ if b = T K ∅ 𝒫 a ∩ Fin ⊆ a
67 66 rabbidva ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin → a ∈ 𝒫 X | T ⊆ a → K ∈ a = a ∈ 𝒫 X | ⋃ b ∈ 𝒫 X ⟼ if b = T K ∅ 𝒫 a ∩ Fin ⊆ a
68 simpll ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin → X ∈ V
69 snelpwi ⊢ K ∈ X → K ∈ 𝒫 X
70 69 ad2antlr ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin → K ∈ 𝒫 X
71 0elpw ⊢ ∅ ∈ 𝒫 X
72 ifcl ⊢ K ∈ 𝒫 X ∧ ∅ ∈ 𝒫 X → if b = T K ∅ ∈ 𝒫 X
73 70 71 72 sylancl ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin → if b = T K ∅ ∈ 𝒫 X
74 73 adantr ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin ∧ b ∈ 𝒫 X → if b = T K ∅ ∈ 𝒫 X
75 74 fmpttd ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin → b ∈ 𝒫 X ⟼ if b = T K ∅ : 𝒫 X ⟶ 𝒫 X
76 isacs1i ⊢ X ∈ V ∧ b ∈ 𝒫 X ⟼ if b = T K ∅ : 𝒫 X ⟶ 𝒫 X → a ∈ 𝒫 X | ⋃ b ∈ 𝒫 X ⟼ if b = T K ∅ 𝒫 a ∩ Fin ⊆ a ∈ ACS ⁡ X
77 68 75 76 syl2anc ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin → a ∈ 𝒫 X | ⋃ b ∈ 𝒫 X ⟼ if b = T K ∅ 𝒫 a ∩ Fin ⊆ a ∈ ACS ⁡ X
78 67 77 eqeltrd ⊢ X ∈ V ∧ K ∈ X ∧ T ⊆ X ∧ T ∈ Fin → a ∈ 𝒫 X | T ⊆ a → K ∈ a ∈ ACS ⁡ X