Metamath Proof Explorer

Theorem fin1a2lem13

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 8-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin1a2lem13 ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A → ¬ B ∖ C ∈ FinII

Proof

Step Hyp Ref Expression
1 simpr ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → B ∖ C ∈ FinII
2 simpll1 ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → A ⊆ 𝒫 B
3 ssel2 ⊢ A ⊆ 𝒫 B ∧ g ∈ A → g ∈ 𝒫 B
4 3 elpwid ⊢ A ⊆ 𝒫 B ∧ g ∈ A → g ⊆ B
5 4 ssdifd ⊢ A ⊆ 𝒫 B ∧ g ∈ A → g ∖ C ⊆ B ∖ C
6 sseq1 ⊢ f = g ∖ C → f ⊆ B ∖ C ↔ g ∖ C ⊆ B ∖ C
7 5 6 syl5ibrcom ⊢ A ⊆ 𝒫 B ∧ g ∈ A → f = g ∖ C → f ⊆ B ∖ C
8 7 rexlimdva ⊢ A ⊆ 𝒫 B → ∃ g ∈ A f = g ∖ C → f ⊆ B ∖ C
9 eqid ⊢ g ∈ A ⟼ g ∖ C = g ∈ A ⟼ g ∖ C
10 9 elrnmpt ⊢ f ∈ V → f ∈ ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∃ g ∈ A f = g ∖ C
11 10 elv ⊢ f ∈ ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∃ g ∈ A f = g ∖ C
12 velpw ⊢ f ∈ 𝒫 B ∖ C ↔ f ⊆ B ∖ C
13 8 11 12 3imtr4g ⊢ A ⊆ 𝒫 B → f ∈ ran ⁡ g ∈ A ⟼ g ∖ C → f ∈ 𝒫 B ∖ C
14 13 ssrdv ⊢ A ⊆ 𝒫 B → ran ⁡ g ∈ A ⟼ g ∖ C ⊆ 𝒫 B ∖ C
15 2 14 syl ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → ran ⁡ g ∈ A ⟼ g ∖ C ⊆ 𝒫 B ∖ C
16 simplrr ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → C ∈ A
17 difid ⊢ C ∖ C = ∅
18 17 eqcomi ⊢ ∅ = C ∖ C
19 difeq1 ⊢ g = C → g ∖ C = C ∖ C
20 19 rspceeqv ⊢ C ∈ A ∧ ∅ = C ∖ C → ∃ g ∈ A ∅ = g ∖ C
21 18 20 mpan2 ⊢ C ∈ A → ∃ g ∈ A ∅ = g ∖ C
22 0ex ⊢ ∅ ∈ V
23 9 elrnmpt ⊢ ∅ ∈ V → ∅ ∈ ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∃ g ∈ A ∅ = g ∖ C
24 22 23 ax-mp ⊢ ∅ ∈ ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∃ g ∈ A ∅ = g ∖ C
25 21 24 sylibr ⊢ C ∈ A → ∅ ∈ ran ⁡ g ∈ A ⟼ g ∖ C
26 ne0i ⊢ ∅ ∈ ran ⁡ g ∈ A ⟼ g ∖ C → ran ⁡ g ∈ A ⟼ g ∖ C ≠ ∅
27 16 25 26 3syl ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → ran ⁡ g ∈ A ⟼ g ∖ C ≠ ∅
28 simpll2 ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → [⊂] Or A
29 9 elrnmpt ⊢ x ∈ V → x ∈ ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∃ g ∈ A x = g ∖ C
30 29 elv ⊢ x ∈ ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∃ g ∈ A x = g ∖ C
31 difeq1 ⊢ g = e → g ∖ C = e ∖ C
32 31 eqeq2d ⊢ g = e → x = g ∖ C ↔ x = e ∖ C
33 32 cbvrexvw ⊢ ∃ g ∈ A x = g ∖ C ↔ ∃ e ∈ A x = e ∖ C
34 sorpssi ⊢ [⊂] Or A ∧ e ∈ A ∧ g ∈ A → e ⊆ g ∨ g ⊆ e
35 ssdif ⊢ e ⊆ g → e ∖ C ⊆ g ∖ C
36 ssdif ⊢ g ⊆ e → g ∖ C ⊆ e ∖ C
37 35 36 orim12i ⊢ e ⊆ g ∨ g ⊆ e → e ∖ C ⊆ g ∖ C ∨ g ∖ C ⊆ e ∖ C
38 34 37 syl ⊢ [⊂] Or A ∧ e ∈ A ∧ g ∈ A → e ∖ C ⊆ g ∖ C ∨ g ∖ C ⊆ e ∖ C
39 sseq2 ⊢ f = g ∖ C → e ∖ C ⊆ f ↔ e ∖ C ⊆ g ∖ C
40 sseq1 ⊢ f = g ∖ C → f ⊆ e ∖ C ↔ g ∖ C ⊆ e ∖ C
41 39 40 orbi12d ⊢ f = g ∖ C → e ∖ C ⊆ f ∨ f ⊆ e ∖ C ↔ e ∖ C ⊆ g ∖ C ∨ g ∖ C ⊆ e ∖ C
42 38 41 syl5ibrcom ⊢ [⊂] Or A ∧ e ∈ A ∧ g ∈ A → f = g ∖ C → e ∖ C ⊆ f ∨ f ⊆ e ∖ C
43 42 expr ⊢ [⊂] Or A ∧ e ∈ A → g ∈ A → f = g ∖ C → e ∖ C ⊆ f ∨ f ⊆ e ∖ C
44 43 rexlimdv ⊢ [⊂] Or A ∧ e ∈ A → ∃ g ∈ A f = g ∖ C → e ∖ C ⊆ f ∨ f ⊆ e ∖ C
45 11 44 biimtrid ⊢ [⊂] Or A ∧ e ∈ A → f ∈ ran ⁡ g ∈ A ⟼ g ∖ C → e ∖ C ⊆ f ∨ f ⊆ e ∖ C
46 45 ralrimiv ⊢ [⊂] Or A ∧ e ∈ A → ∀ f ∈ ran ⁡ g ∈ A ⟼ g ∖ C e ∖ C ⊆ f ∨ f ⊆ e ∖ C
47 sseq1 ⊢ x = e ∖ C → x ⊆ f ↔ e ∖ C ⊆ f
48 sseq2 ⊢ x = e ∖ C → f ⊆ x ↔ f ⊆ e ∖ C
49 47 48 orbi12d ⊢ x = e ∖ C → x ⊆ f ∨ f ⊆ x ↔ e ∖ C ⊆ f ∨ f ⊆ e ∖ C
50 49 ralbidv ⊢ x = e ∖ C → ∀ f ∈ ran ⁡ g ∈ A ⟼ g ∖ C x ⊆ f ∨ f ⊆ x ↔ ∀ f ∈ ran ⁡ g ∈ A ⟼ g ∖ C e ∖ C ⊆ f ∨ f ⊆ e ∖ C
51 46 50 syl5ibrcom ⊢ [⊂] Or A ∧ e ∈ A → x = e ∖ C → ∀ f ∈ ran ⁡ g ∈ A ⟼ g ∖ C x ⊆ f ∨ f ⊆ x
52 51 rexlimdva ⊢ [⊂] Or A → ∃ e ∈ A x = e ∖ C → ∀ f ∈ ran ⁡ g ∈ A ⟼ g ∖ C x ⊆ f ∨ f ⊆ x
53 33 52 biimtrid ⊢ [⊂] Or A → ∃ g ∈ A x = g ∖ C → ∀ f ∈ ran ⁡ g ∈ A ⟼ g ∖ C x ⊆ f ∨ f ⊆ x
54 30 53 biimtrid ⊢ [⊂] Or A → x ∈ ran ⁡ g ∈ A ⟼ g ∖ C → ∀ f ∈ ran ⁡ g ∈ A ⟼ g ∖ C x ⊆ f ∨ f ⊆ x
55 54 ralrimiv ⊢ [⊂] Or A → ∀ x ∈ ran ⁡ g ∈ A ⟼ g ∖ C ∀ f ∈ ran ⁡ g ∈ A ⟼ g ∖ C x ⊆ f ∨ f ⊆ x
56 sorpss ⊢ [⊂] Or ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∀ x ∈ ran ⁡ g ∈ A ⟼ g ∖ C ∀ f ∈ ran ⁡ g ∈ A ⟼ g ∖ C x ⊆ f ∨ f ⊆ x
57 55 56 sylibr ⊢ [⊂] Or A → [⊂] Or ran ⁡ g ∈ A ⟼ g ∖ C
58 28 57 syl ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → [⊂] Or ran ⁡ g ∈ A ⟼ g ∖ C
59 fin2i ⊢ B ∖ C ∈ FinII ∧ ran ⁡ g ∈ A ⟼ g ∖ C ⊆ 𝒫 B ∖ C ∧ ran ⁡ g ∈ A ⟼ g ∖ C ≠ ∅ ∧ [⊂] Or ran ⁡ g ∈ A ⟼ g ∖ C → ⋃ ran ⁡ g ∈ A ⟼ g ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C
60 1 15 27 58 59 syl22anc ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → ⋃ ran ⁡ g ∈ A ⟼ g ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C
61 simpll3 ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → ¬ ⋃ A ∈ A
62 difeq1 ⊢ g = f → g ∖ C = f ∖ C
63 62 cbvmptv ⊢ g ∈ A ⟼ g ∖ C = f ∈ A ⟼ f ∖ C
64 63 elrnmpt ⊢ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C → ⋃ ran ⁡ g ∈ A ⟼ g ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∃ f ∈ A ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C
65 64 ibi ⊢ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C → ∃ f ∈ A ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C
66 eqid ⊢ h ∖ C = h ∖ C
67 difeq1 ⊢ g = h → g ∖ C = h ∖ C
68 67 rspceeqv ⊢ h ∈ A ∧ h ∖ C = h ∖ C → ∃ g ∈ A h ∖ C = g ∖ C
69 66 68 mpan2 ⊢ h ∈ A → ∃ g ∈ A h ∖ C = g ∖ C
70 69 adantl ⊢ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → ∃ g ∈ A h ∖ C = g ∖ C
71 vex ⊢ h ∈ V
72 difexg ⊢ h ∈ V → h ∖ C ∈ V
73 9 elrnmpt ⊢ h ∖ C ∈ V → h ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∃ g ∈ A h ∖ C = g ∖ C
74 71 72 73 mp2b ⊢ h ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∃ g ∈ A h ∖ C = g ∖ C
75 70 74 sylibr ⊢ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → h ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C
76 elssuni ⊢ h ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C → h ∖ C ⊆ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C
77 75 76 syl ⊢ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → h ∖ C ⊆ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C
78 simplr ⊢ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C
79 77 78 sseqtrd ⊢ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → h ∖ C ⊆ f ∖ C
80 79 adantll ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → h ∖ C ⊆ f ∖ C
81 unss2 ⊢ h ∖ C ⊆ f ∖ C → C ∪ h ∖ C ⊆ C ∪ f ∖ C
82 uncom ⊢ C ∪ h ∖ C = h ∖ C ∪ C
83 undif1 ⊢ h ∖ C ∪ C = h ∪ C
84 82 83 eqtri ⊢ C ∪ h ∖ C = h ∪ C
85 84 a1i ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → C ∪ h ∖ C = h ∪ C
86 61 ad2antrr ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → ¬ ⋃ A ∈ A
87 16 ad2antrr ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → C ∈ A
88 simplrr ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C
89 eqeq1 ⊢ e = x ∖ C → e = ∅ ↔ x ∖ C = ∅
90 simpllr ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C ∧ x ∈ A → ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C
91 ssdif0 ⊢ f ⊆ C ↔ f ∖ C = ∅
92 91 biimpi ⊢ f ⊆ C → f ∖ C = ∅
93 92 ad2antlr ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C ∧ x ∈ A → f ∖ C = ∅
94 90 93 eqtrd ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C ∧ x ∈ A → ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = ∅
95 uni0c ⊢ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = ∅ ↔ ∀ e ∈ ran ⁡ g ∈ A ⟼ g ∖ C e = ∅
96 94 95 sylib ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C ∧ x ∈ A → ∀ e ∈ ran ⁡ g ∈ A ⟼ g ∖ C e = ∅
97 eqid ⊢ x ∖ C = x ∖ C
98 difeq1 ⊢ g = x → g ∖ C = x ∖ C
99 98 rspceeqv ⊢ x ∈ A ∧ x ∖ C = x ∖ C → ∃ g ∈ A x ∖ C = g ∖ C
100 97 99 mpan2 ⊢ x ∈ A → ∃ g ∈ A x ∖ C = g ∖ C
101 vex ⊢ x ∈ V
102 difexg ⊢ x ∈ V → x ∖ C ∈ V
103 9 elrnmpt ⊢ x ∖ C ∈ V → x ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∃ g ∈ A x ∖ C = g ∖ C
104 101 102 103 mp2b ⊢ x ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C ↔ ∃ g ∈ A x ∖ C = g ∖ C
105 100 104 sylibr ⊢ x ∈ A → x ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C
106 105 adantl ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C ∧ x ∈ A → x ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C
107 89 96 106 rspcdva ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C ∧ x ∈ A → x ∖ C = ∅
108 ssdif0 ⊢ x ⊆ C ↔ x ∖ C = ∅
109 107 108 sylibr ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C ∧ x ∈ A → x ⊆ C
110 109 ralrimiva ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C → ∀ x ∈ A x ⊆ C
111 unissb ⊢ ⋃ A ⊆ C ↔ ∀ x ∈ A x ⊆ C
112 110 111 sylibr ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C → ⋃ A ⊆ C
113 elssuni ⊢ C ∈ A → C ⊆ ⋃ A
114 113 ad2antrr ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C → C ⊆ ⋃ A
115 112 114 eqssd ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C → ⋃ A = C
116 simpll ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C → C ∈ A
117 115 116 eqeltrd ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ f ⊆ C → ⋃ A ∈ A
118 117 ex ⊢ C ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C → f ⊆ C → ⋃ A ∈ A
119 87 88 118 syl2anc ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → f ⊆ C → ⋃ A ∈ A
120 86 119 mtod ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → ¬ f ⊆ C
121 28 ad2antrr ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → [⊂] Or A
122 simplrl ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → f ∈ A
123 sorpssi ⊢ [⊂] Or A ∧ f ∈ A ∧ C ∈ A → f ⊆ C ∨ C ⊆ f
124 121 122 87 123 syl12anc ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → f ⊆ C ∨ C ⊆ f
125 orel1 ⊢ ¬ f ⊆ C → f ⊆ C ∨ C ⊆ f → C ⊆ f
126 120 124 125 sylc ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → C ⊆ f
127 undif ⊢ C ⊆ f ↔ C ∪ f ∖ C = f
128 126 127 sylib ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → C ∪ f ∖ C = f
129 85 128 sseq12d ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → C ∪ h ∖ C ⊆ C ∪ f ∖ C ↔ h ∪ C ⊆ f
130 ssun1 ⊢ h ⊆ h ∪ C
131 sstr ⊢ h ⊆ h ∪ C ∧ h ∪ C ⊆ f → h ⊆ f
132 130 131 mpan ⊢ h ∪ C ⊆ f → h ⊆ f
133 129 132 biimtrdi ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → C ∪ h ∖ C ⊆ C ∪ f ∖ C → h ⊆ f
134 81 133 syl5 ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → h ∖ C ⊆ f ∖ C → h ⊆ f
135 80 134 mpd ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C ∧ h ∈ A → h ⊆ f
136 135 ralrimiva ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C → ∀ h ∈ A h ⊆ f
137 unissb ⊢ ⋃ A ⊆ f ↔ ∀ h ∈ A h ⊆ f
138 136 137 sylibr ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C → ⋃ A ⊆ f
139 elssuni ⊢ f ∈ A → f ⊆ ⋃ A
140 139 ad2antrl ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C → f ⊆ ⋃ A
141 138 140 eqssd ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C → ⋃ A = f
142 simprl ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C → f ∈ A
143 141 142 eqeltrd ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII ∧ f ∈ A ∧ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C → ⋃ A ∈ A
144 143 rexlimdvaa ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → ∃ f ∈ A ⋃ ran ⁡ g ∈ A ⟼ g ∖ C = f ∖ C → ⋃ A ∈ A
145 65 144 syl5 ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → ⋃ ran ⁡ g ∈ A ⟼ g ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C → ⋃ A ∈ A
146 61 145 mtod ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A ∧ B ∖ C ∈ FinII → ¬ ⋃ ran ⁡ g ∈ A ⟼ g ∖ C ∈ ran ⁡ g ∈ A ⟼ g ∖ C
147 60 146 pm2.65da ⊢ A ⊆ 𝒫 B ∧ [⊂] Or A ∧ ¬ ⋃ A ∈ A ∧ ¬ C ∈ Fin ∧ C ∈ A → ¬ B ∖ C ∈ FinII