MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ttukeylem6 Structured version   Visualization version   GIF version

Theorem ttukeylem6 10451
Description: Lemma for ttukey 10455. (Contributed by Mario Carneiro, 15-May-2015.)
Hypotheses
Ref Expression
ttukeylem.1 (πœ‘ β†’ 𝐹:(cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))–1-1-ontoβ†’(βˆͺ 𝐴 βˆ– 𝐡))
ttukeylem.2 (πœ‘ β†’ 𝐡 ∈ 𝐴)
ttukeylem.3 (πœ‘ β†’ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴))
ttukeylem.4 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…)))))
Assertion
Ref Expression
ttukeylem6 ((πœ‘ ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (πΊβ€˜πΆ) ∈ 𝐴)
Distinct variable groups:   π‘₯,𝑧,𝐢   π‘₯,𝐺,𝑧   πœ‘,𝑧   π‘₯,𝐴,𝑧   π‘₯,𝐡,𝑧   π‘₯,𝐹,𝑧
Allowed substitution hint:   πœ‘(π‘₯)

Proof of Theorem ttukeylem6
Dummy variables π‘Ž 𝑦 𝑓 𝑒 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cardon 9881 . . . . 5 (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On
21onsuci 7775 . . . 4 suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On
32a1i 11 . . 3 (πœ‘ β†’ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On)
4 onelon 6343 . . 3 ((suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝐢 ∈ On)
53, 4sylan 581 . 2 ((πœ‘ ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝐢 ∈ On)
6 eleq1 2826 . . . . . 6 (𝑦 = π‘Ž β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ↔ π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))))
7 fveq2 6843 . . . . . . 7 (𝑦 = π‘Ž β†’ (πΊβ€˜π‘¦) = (πΊβ€˜π‘Ž))
87eleq1d 2823 . . . . . 6 (𝑦 = π‘Ž β†’ ((πΊβ€˜π‘¦) ∈ 𝐴 ↔ (πΊβ€˜π‘Ž) ∈ 𝐴))
96, 8imbi12d 345 . . . . 5 (𝑦 = π‘Ž β†’ ((𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴) ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
109imbi2d 341 . . . 4 (𝑦 = π‘Ž β†’ ((πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)) ↔ (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴))))
11 eleq1 2826 . . . . . 6 (𝑦 = 𝐢 β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ↔ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))))
12 fveq2 6843 . . . . . . 7 (𝑦 = 𝐢 β†’ (πΊβ€˜π‘¦) = (πΊβ€˜πΆ))
1312eleq1d 2823 . . . . . 6 (𝑦 = 𝐢 β†’ ((πΊβ€˜π‘¦) ∈ 𝐴 ↔ (πΊβ€˜πΆ) ∈ 𝐴))
1411, 13imbi12d 345 . . . . 5 (𝑦 = 𝐢 β†’ ((𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴) ↔ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴)))
1514imbi2d 341 . . . 4 (𝑦 = 𝐢 β†’ ((πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)) ↔ (πœ‘ β†’ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴))))
16 r19.21v 3177 . . . . . 6 (βˆ€π‘Ž ∈ 𝑦 (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)) ↔ (πœ‘ β†’ βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
172onordi 6429 . . . . . . . . . . . . . . 15 Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))
1817a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
19 ordelss 6334 . . . . . . . . . . . . . 14 ((Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝑦 βŠ† suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2018, 19sylan 581 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝑦 βŠ† suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2120sselda 3945 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) ∧ π‘Ž ∈ 𝑦) β†’ π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
22 biimt 361 . . . . . . . . . . . 12 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
2321, 22syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) ∧ π‘Ž ∈ 𝑦) β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
2423ralbidva 3173 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴 ↔ βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
252onssi 7774 . . . . . . . . . . . . . 14 suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) βŠ† On
26 simprl 770 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2725, 26sselid 3943 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ 𝑦 ∈ On)
28 ttukeylem.1 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐹:(cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))–1-1-ontoβ†’(βˆͺ 𝐴 βˆ– 𝐡))
29 ttukeylem.2 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐡 ∈ 𝐴)
30 ttukeylem.3 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ (𝒫 π‘₯ ∩ Fin) βŠ† 𝐴))
31 ttukeylem.4 . . . . . . . . . . . . . 14 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…)))))
3228, 29, 30, 31ttukeylem3 10448 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ On) β†’ (πΊβ€˜π‘¦) = if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))))
3327, 32syldan 592 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (πΊβ€˜π‘¦) = if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))))
3429ad3antrrr 729 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑦 = βˆ…) β†’ 𝐡 ∈ 𝐴)
35 simpr 486 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin))
3635elin2d 4160 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ Fin)
3735elin1d 4159 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ 𝒫 βˆͺ (𝐺 β€œ 𝑦))
3837elpwid 4570 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 βŠ† βˆͺ (𝐺 β€œ 𝑦))
3931tfr1 8344 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 Fn On
40 fnfun 6603 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn On β†’ Fun 𝐺)
41 funiunfv 7196 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐺 β†’ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) = βˆͺ (𝐺 β€œ 𝑦))
4239, 40, 41mp2b 10 . . . . . . . . . . . . . . . . . . . . . 22 βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) = βˆͺ (𝐺 β€œ 𝑦)
4338, 42sseqtrrdi 3996 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£))
44 dfss3 3933 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£))
45 eliun 4959 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4645ralbii 3097 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘’ ∈ 𝑀 𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4744, 46bitri 275 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4843, 47sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
49 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (π‘“β€˜π‘’) β†’ (πΊβ€˜π‘£) = (πΊβ€˜(π‘“β€˜π‘’)))
5049eleq2d 2824 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (π‘“β€˜π‘’) β†’ (𝑒 ∈ (πΊβ€˜π‘£) ↔ 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
5150ac6sfi 9232 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ Fin ∧ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£)) β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
5236, 48, 51syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
53 eleq1 2826 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 = βˆ… β†’ (𝑀 ∈ 𝐴 ↔ βˆ… ∈ 𝐴))
54 simp-4l 782 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ πœ‘)
55 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž = βˆͺ ran 𝑓 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜βˆͺ ran 𝑓))
5655eleq1d 2823 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž = βˆͺ ran 𝑓 β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴))
57 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
5857ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
59 simprrl 780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑓:π‘€βŸΆπ‘¦)
6059adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓:π‘€βŸΆπ‘¦)
61 frn 6676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:π‘€βŸΆπ‘¦ β†’ ran 𝑓 βŠ† 𝑦)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 βŠ† 𝑦)
6327ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑦 ∈ On)
64 onss 7720 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ On β†’ 𝑦 βŠ† On)
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑦 βŠ† On)
6662, 65sstrd 3955 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 βŠ† On)
6736adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑀 ∈ Fin)
6867adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 ∈ Fin)
69 ffn 6669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:π‘€βŸΆπ‘¦ β†’ 𝑓 Fn 𝑀)
7060, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓 Fn 𝑀)
71 dffn4 6763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 Fn 𝑀 ↔ 𝑓:𝑀–ontoβ†’ran 𝑓)
7270, 71sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓:𝑀–ontoβ†’ran 𝑓)
73 fofi 9283 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑀 ∈ Fin ∧ 𝑓:𝑀–ontoβ†’ran 𝑓) β†’ ran 𝑓 ∈ Fin)
7468, 72, 73syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 ∈ Fin)
75 dm0rn0 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑓 = βˆ… ↔ ran 𝑓 = βˆ…)
7659fdmd 6680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ dom 𝑓 = 𝑀)
7776eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (dom 𝑓 = βˆ… ↔ 𝑀 = βˆ…))
7875, 77bitr3id 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (ran 𝑓 = βˆ… ↔ 𝑀 = βˆ…))
7978necon3bid 2989 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (ran 𝑓 β‰  βˆ… ↔ 𝑀 β‰  βˆ…))
8079biimpar 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 β‰  βˆ…)
81 ordunifi 9238 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran 𝑓 βŠ† On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ ran 𝑓)
8266, 74, 80, 81syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ ran 𝑓)
8362, 82sseldd 3946 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ 𝑦)
8456, 58, 83rspcdva 3583 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ (πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴)
85 simp-4l 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ πœ‘)
8627ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑦 ∈ On)
8786, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑦 βŠ† On)
88 ffvelcdm 7033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀) β†’ (π‘“β€˜π‘’) ∈ 𝑦)
8988adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ 𝑦)
9087, 89sseldd 3946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ On)
9161ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ ran 𝑓 βŠ† 𝑦)
9291, 87sstrd 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ ran 𝑓 βŠ† On)
93 vex 3450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑓 ∈ V
9493rnex 7850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran 𝑓 ∈ V
9594ssonunii 7716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ran 𝑓 βŠ† On β†’ βˆͺ ran 𝑓 ∈ On)
9692, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ βˆͺ ran 𝑓 ∈ On)
9769ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑓 Fn 𝑀)
98 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑒 ∈ 𝑀)
99 fnfvelrn 7032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 Fn 𝑀 ∧ 𝑒 ∈ 𝑀) β†’ (π‘“β€˜π‘’) ∈ ran 𝑓)
10097, 98, 99syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ ran 𝑓)
101 elssuni 4899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((π‘“β€˜π‘’) ∈ ran 𝑓 β†’ (π‘“β€˜π‘’) βŠ† βˆͺ ran 𝑓)
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) βŠ† βˆͺ ran 𝑓)
10328, 29, 30, 31ttukeylem5 10450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ ((π‘“β€˜π‘’) ∈ On ∧ βˆͺ ran 𝑓 ∈ On ∧ (π‘“β€˜π‘’) βŠ† βˆͺ ran 𝑓)) β†’ (πΊβ€˜(π‘“β€˜π‘’)) βŠ† (πΊβ€˜βˆͺ ran 𝑓))
10485, 90, 96, 102, 103syl13anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (πΊβ€˜(π‘“β€˜π‘’)) βŠ† (πΊβ€˜βˆͺ ran 𝑓))
105104sseld 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
106105anassrs 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ 𝑓:π‘€βŸΆπ‘¦) ∧ 𝑒 ∈ 𝑀) β†’ (𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
107106ralimdva 3165 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ 𝑓:π‘€βŸΆπ‘¦) β†’ (βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
108107expimpd 455 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ ((𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
109108impr 456 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
110109adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
111 dfss3 3933 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓) ↔ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
112110, 111sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓))
11328, 29, 30ttukeylem2 10447 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ ((πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴 ∧ 𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓))) β†’ 𝑀 ∈ 𝐴)
11454, 84, 112, 113syl12anc 836 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 ∈ 𝐴)
115 0ss 4357 . . . . . . . . . . . . . . . . . . . . . . . . 25 βˆ… βŠ† 𝐡
11628, 29, 30ttukeylem2 10447 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝐡 ∈ 𝐴 ∧ βˆ… βŠ† 𝐡)) β†’ βˆ… ∈ 𝐴)
117115, 116mpanr2 703 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝐡 ∈ 𝐴) β†’ βˆ… ∈ 𝐴)
11829, 117mpdan 686 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆ… ∈ 𝐴)
119118ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ βˆ… ∈ 𝐴)
12053, 114, 119pm2.61ne 3031 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑀 ∈ 𝐴)
121120expr 458 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ ((𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ 𝑀 ∈ 𝐴))
122121exlimdv 1937 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ 𝑀 ∈ 𝐴))
12352, 122mpd 15 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ 𝐴)
124123ex 414 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) β†’ 𝑀 ∈ 𝐴))
125124ssrdv 3951 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴)
12628, 29, 30ttukeylem1 10446 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴 ↔ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴))
127126ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴 ↔ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴))
128125, 127mpbird 257 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴)
129128adantr 482 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ Β¬ 𝑦 = βˆ…) β†’ βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴)
13034, 129ifclda 4522 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)) ∈ 𝐴)
131 uneq2 4118 . . . . . . . . . . . . . . 15 ({(πΉβ€˜βˆͺ 𝑦)} = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
132131eleq1d 2823 . . . . . . . . . . . . . 14 ({(πΉβ€˜βˆͺ 𝑦)} = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ (((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴))
133 un0 4351 . . . . . . . . . . . . . . . 16 ((πΊβ€˜βˆͺ 𝑦) βˆͺ βˆ…) = (πΊβ€˜βˆͺ 𝑦)
134 uneq2 4118 . . . . . . . . . . . . . . . 16 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ βˆ…) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
135133, 134eqtr3id 2791 . . . . . . . . . . . . . . 15 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ (πΊβ€˜βˆͺ 𝑦) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
136135eleq1d 2823 . . . . . . . . . . . . . 14 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴))
137 simpr 486 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) ∧ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴)
138 fveq2 6843 . . . . . . . . . . . . . . . . 17 (π‘Ž = βˆͺ 𝑦 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜βˆͺ 𝑦))
139138eleq1d 2823 . . . . . . . . . . . . . . . 16 (π‘Ž = βˆͺ 𝑦 β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴))
140 simplrr 777 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
141 vuniex 7677 . . . . . . . . . . . . . . . . . 18 βˆͺ 𝑦 ∈ V
142141sucid 6400 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑦 ∈ suc βˆͺ 𝑦
143 eloni 6328 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On β†’ Ord 𝑦)
144 orduniorsuc 7766 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑦 β†’ (𝑦 = βˆͺ 𝑦 ∨ 𝑦 = suc βˆͺ 𝑦))
14527, 143, 1443syl 18 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (𝑦 = βˆͺ 𝑦 ∨ 𝑦 = suc βˆͺ 𝑦))
146145orcanai 1002 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ 𝑦 = suc βˆͺ 𝑦)
147142, 146eleqtrrid 2845 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ βˆͺ 𝑦 ∈ 𝑦)
148139, 140, 147rspcdva 3583 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴)
149148adantr 482 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) ∧ Β¬ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴) β†’ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴)
150132, 136, 137, 149ifbothda 4525 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴)
151130, 150ifclda 4522 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))) ∈ 𝐴)
15233, 151eqeltrd 2838 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)
153152expr 458 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴 β†’ (πΊβ€˜π‘¦) ∈ 𝐴))
15424, 153sylbird 260 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴) β†’ (πΊβ€˜π‘¦) ∈ 𝐴))
155154ex 414 . . . . . . . 8 (πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)))
156155com23 86 . . . . . . 7 (πœ‘ β†’ (βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴) β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)))
157156a2i 14 . . . . . 6 ((πœ‘ β†’ βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)))
15816, 157sylbi 216 . . . . 5 (βˆ€π‘Ž ∈ 𝑦 (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)))
159158a1i 11 . . . 4 (𝑦 ∈ On β†’ (βˆ€π‘Ž ∈ 𝑦 (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴))))
16010, 15, 159tfis3 7795 . . 3 (𝐢 ∈ On β†’ (πœ‘ β†’ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴)))
161160impd 412 . 2 (𝐢 ∈ On β†’ ((πœ‘ ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (πΊβ€˜πΆ) ∈ 𝐴))
1625, 161mpcom 38 1 ((πœ‘ ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (πΊβ€˜πΆ) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846  βˆ€wal 1540   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3446   βˆ– cdif 3908   βˆͺ cun 3909   ∩ cin 3910   βŠ† wss 3911  βˆ…c0 4283  ifcif 4487  π’« cpw 4561  {csn 4587  βˆͺ cuni 4866  βˆͺ ciun 4955   ↦ cmpt 5189  dom cdm 5634  ran crn 5635   β€œ cima 5637  Ord word 6317  Oncon0 6318  suc csuc 6320  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493  β€“ontoβ†’wfo 6495  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497  recscrecs 8317  Fincfn 8884  cardccrd 9872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-1o 8413  df-er 8649  df-en 8885  df-dom 8886  df-fin 8888  df-card 9876
This theorem is referenced by:  ttukeylem7  10452
  Copyright terms: Public domain W3C validator