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∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A→¬B∖C∈FinII

Proof

Step Hyp Ref Expression
1 simpr ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A∧B∖C∈FinII→B∖C∈FinII
2 simpll1 ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃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∈Af=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∈Af=g∖C
11 10 elv ⊢f∈ran⁡g∈A⟼g∖C↔∃g∈Af=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∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A∧B∖C∈FinII→ran⁡g∈A⟼g∖C⊆𝒫B∖C
16 simplrr ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A∧B∖C∈FinII→ran⁡g∈A⟼g∖C≠∅
28 simpll2 ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A∧B∖C∈FinII→[⊂]OrA
29 9 elrnmpt ⊢x∈V→x∈ran⁡g∈A⟼g∖C↔∃g∈Ax=g∖C
30 29 elv ⊢x∈ran⁡g∈A⟼g∖C↔∃g∈Ax=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∈Ax=g∖C↔∃e∈Ax=e∖C
34 sorpssi ⊢[⊂]OrA∧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 ⊢[⊂]OrA∧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 ⊢[⊂]OrA∧e∈A∧g∈A→f=g∖C→e∖C⊆f∨f⊆e∖C
43 42 expr ⊢[⊂]OrA∧e∈A→g∈A→f=g∖C→e∖C⊆f∨f⊆e∖C
44 43 rexlimdv ⊢[⊂]OrA∧e∈A→∃g∈Af=g∖C→e∖C⊆f∨f⊆e∖C
45 11 44 biimtrid ⊢[⊂]OrA∧e∈A→f∈ran⁡g∈A⟼g∖C→e∖C⊆f∨f⊆e∖C
46 45 ralrimiv ⊢[⊂]OrA∧e∈A→∀f∈ran⁡g∈A⟼g∖Ce∖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∖Cx⊆f∨f⊆x↔∀f∈ran⁡g∈A⟼g∖Ce∖C⊆f∨f⊆e∖C
51 46 50 syl5ibrcom ⊢[⊂]OrA∧e∈A→x=e∖C→∀f∈ran⁡g∈A⟼g∖Cx⊆f∨f⊆x
52 51 rexlimdva ⊢[⊂]OrA→∃e∈Ax=e∖C→∀f∈ran⁡g∈A⟼g∖Cx⊆f∨f⊆x
53 33 52 biimtrid ⊢[⊂]OrA→∃g∈Ax=g∖C→∀f∈ran⁡g∈A⟼g∖Cx⊆f∨f⊆x
54 30 53 biimtrid ⊢[⊂]OrA→x∈ran⁡g∈A⟼g∖C→∀f∈ran⁡g∈A⟼g∖Cx⊆f∨f⊆x
55 54 ralrimiv ⊢[⊂]OrA→∀x∈ran⁡g∈A⟼g∖C∀f∈ran⁡g∈A⟼g∖Cx⊆f∨f⊆x
56 sorpss ⊢[⊂]Orran⁡g∈A⟼g∖C↔∀x∈ran⁡g∈A⟼g∖C∀f∈ran⁡g∈A⟼g∖Cx⊆f∨f⊆x
57 55 56 sylibr ⊢[⊂]OrA→[⊂]Orran⁡g∈A⟼g∖C
58 28 57 syl ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A∧B∖C∈FinII→[⊂]Orran⁡g∈A⟼g∖C
59 fin2i ⊢B∖C∈FinII∧ran⁡g∈A⟼g∖C⊆𝒫B∖C∧ran⁡g∈A⟼g∖C≠∅∧[⊂]Orran⁡g∈A⟼g∖C→⋃ran⁡g∈A⟼g∖C∈ran⁡g∈A⟼g∖C
60 1 15 27 58 59 syl22anc ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A∧B∖C∈FinII→⋃ran⁡g∈A⟼g∖C∈ran⁡g∈A⟼g∖C
61 simpll3 ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃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∈Ah∖C=g∖C
69 66 68 mpan2 ⊢h∈A→∃g∈Ah∖C=g∖C
70 69 adantl ⊢f∈A∧⋃ran⁡g∈A⟼g∖C=f∖C∧h∈A→∃g∈Ah∖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∈Ah∖C=g∖C
74 71 72 73 mp2b ⊢h∖C∈ran⁡g∈A⟼g∖C↔∃g∈Ah∖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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∖Ce=∅
96 94 95 sylib ⊢C∈A∧⋃ran⁡g∈A⟼g∖C=f∖C∧f⊆C∧x∈A→∀e∈ran⁡g∈A⟼g∖Ce=∅
97 eqid ⊢x∖C=x∖C
98 difeq1 ⊢g=x→g∖C=x∖C
99 98 rspceeqv ⊢x∈A∧x∖C=x∖C→∃g∈Ax∖C=g∖C
100 97 99 mpan2 ⊢x∈A→∃g∈Ax∖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∈Ax∖C=g∖C
104 101 102 103 mp2b ⊢x∖C∈ran⁡g∈A⟼g∖C↔∃g∈Ax∖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∈Ax⊆C
111 unissb ⊢⋃A⊆C↔∀x∈Ax⊆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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A∧B∖C∈FinII∧f∈A∧⋃ran⁡g∈A⟼g∖C=f∖C∧h∈A→[⊂]OrA
122 simplrl ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A∧B∖C∈FinII∧f∈A∧⋃ran⁡g∈A⟼g∖C=f∖C∧h∈A→f∈A
123 sorpssi ⊢[⊂]OrA∧f∈A∧C∈A→f⊆C∨C⊆f
124 121 122 87 123 syl12anc ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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 syl6bi ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A∧B∖C∈FinII∧f∈A∧⋃ran⁡g∈A⟼g∖C=f∖C→∀h∈Ah⊆f
137 unissb ⊢⋃A⊆f↔∀h∈Ah⊆f
138 136 137 sylibr ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A∧B∖C∈FinII∧f∈A∧⋃ran⁡g∈A⟼g∖C=f∖C→⋃A=f
142 simprl ⊢A⊆𝒫B∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃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∧[⊂]OrA∧¬⋃A∈A∧¬C∈Fin∧C∈A→¬B∖C∈FinII