MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ttukeylem6 Structured version   Visualization version   GIF version
Theorem ttukeylem6 10505
Description: Lemma for ttukey 10509. (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 9935 . . . . 5 (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On
21onsuci 7820 . . . 4 suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On
32a1i 11 . . 3 (πœ‘ β†’ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On)
4 onelon 6379 . . 3 ((suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝐢 ∈ On)
53, 4sylan 579 . 2 ((πœ‘ ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝐢 ∈ On)
6 eleq1 2813 . . . . . 6 (𝑦 = π‘Ž β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ↔ π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))))
7 fveq2 6881 . . . . . . 7 (𝑦 = π‘Ž β†’ (πΊβ€˜π‘¦) = (πΊβ€˜π‘Ž))
87eleq1d 2810 . . . . . 6 (𝑦 = π‘Ž β†’ ((πΊβ€˜π‘¦) ∈ 𝐴 ↔ (πΊβ€˜π‘Ž) ∈ 𝐴))
96, 8imbi12d 344 . . . . 5 (𝑦 = π‘Ž β†’ ((𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴) ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
109imbi2d 340 . . . 4 (𝑦 = π‘Ž β†’ ((πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)) ↔ (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴))))
11 eleq1 2813 . . . . . 6 (𝑦 = 𝐢 β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ↔ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))))
12 fveq2 6881 . . . . . . 7 (𝑦 = 𝐢 β†’ (πΊβ€˜π‘¦) = (πΊβ€˜πΆ))
1312eleq1d 2810 . . . . . 6 (𝑦 = 𝐢 β†’ ((πΊβ€˜π‘¦) ∈ 𝐴 ↔ (πΊβ€˜πΆ) ∈ 𝐴))
1411, 13imbi12d 344 . . . . 5 (𝑦 = 𝐢 β†’ ((𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴) ↔ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴)))
1514imbi2d 340 . . . 4 (𝑦 = 𝐢 β†’ ((πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)) ↔ (πœ‘ β†’ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴))))
16 r19.21v 3171 . . . . . 6 (βˆ€π‘Ž ∈ 𝑦 (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)) ↔ (πœ‘ β†’ βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
172onordi 6465 . . . . . . . . . . . . . . 15 Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))
1817a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
19 ordelss 6370 . . . . . . . . . . . . . 14 ((Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝑦 βŠ† suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2018, 19sylan 579 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝑦 βŠ† suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2120sselda 3974 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) ∧ π‘Ž ∈ 𝑦) β†’ π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
22 biimt 360 . . . . . . . . . . . 12 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
2321, 22syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) ∧ π‘Ž ∈ 𝑦) β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
2423ralbidva 3167 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴 ↔ βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
252onssi 7819 . . . . . . . . . . . . . 14 suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) βŠ† On
26 simprl 768 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2725, 26sselid 3972 . . . . . . . . . . . . 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 10502 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ On) β†’ (πΊβ€˜π‘¦) = if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))))
3327, 32syldan 590 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (πΊβ€˜π‘¦) = if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))))
3429ad3antrrr 727 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑦 = βˆ…) β†’ 𝐡 ∈ 𝐴)
35 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin))
3635elin2d 4191 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ Fin)
3735elin1d 4190 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ 𝒫 βˆͺ (𝐺 β€œ 𝑦))
3837elpwid 4603 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 βŠ† βˆͺ (𝐺 β€œ 𝑦))
3931tfr1 8392 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 Fn On
40 fnfun 6639 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn On β†’ Fun 𝐺)
41 funiunfv 7239 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐺 β†’ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) = βˆͺ (𝐺 β€œ 𝑦))
4239, 40, 41mp2b 10 . . . . . . . . . . . . . . . . . . . . . 22 βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) = βˆͺ (𝐺 β€œ 𝑦)
4338, 42sseqtrrdi 4025 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£))
44 dfss3 3962 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£))
45 eliun 4991 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4645ralbii 3085 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘’ ∈ 𝑀 𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4744, 46bitri 275 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4843, 47sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
49 fveq2 6881 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (π‘“β€˜π‘’) β†’ (πΊβ€˜π‘£) = (πΊβ€˜(π‘“β€˜π‘’)))
5049eleq2d 2811 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (π‘“β€˜π‘’) β†’ (𝑒 ∈ (πΊβ€˜π‘£) ↔ 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
5150ac6sfi 9283 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ Fin ∧ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£)) β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
5236, 48, 51syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
53 eleq1 2813 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 = βˆ… β†’ (𝑀 ∈ 𝐴 ↔ βˆ… ∈ 𝐴))
54 simp-4l 780 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ πœ‘)
55 fveq2 6881 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž = βˆͺ ran 𝑓 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜βˆͺ ran 𝑓))
5655eleq1d 2810 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž = βˆͺ ran 𝑓 β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴))
57 simplrr 775 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
5857ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
59 simprrl 778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑓:π‘€βŸΆπ‘¦)
6059adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓:π‘€βŸΆπ‘¦)
61 frn 6714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:π‘€βŸΆπ‘¦ β†’ ran 𝑓 βŠ† 𝑦)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 βŠ† 𝑦)
6327ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑦 ∈ On)
64 onss 7765 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ On β†’ 𝑦 βŠ† On)
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑦 βŠ† On)
6662, 65sstrd 3984 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 βŠ† On)
6736adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑀 ∈ Fin)
6867adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 ∈ Fin)
69 ffn 6707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:π‘€βŸΆπ‘¦ β†’ 𝑓 Fn 𝑀)
7060, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓 Fn 𝑀)
71 dffn4 6801 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 Fn 𝑀 ↔ 𝑓:𝑀–ontoβ†’ran 𝑓)
7270, 71sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓:𝑀–ontoβ†’ran 𝑓)
73 fofi 9334 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑀 ∈ Fin ∧ 𝑓:𝑀–ontoβ†’ran 𝑓) β†’ ran 𝑓 ∈ Fin)
7468, 72, 73syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 ∈ Fin)
75 dm0rn0 5914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑓 = βˆ… ↔ ran 𝑓 = βˆ…)
7659fdmd 6718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ dom 𝑓 = 𝑀)
7776eqeq1d 2726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (dom 𝑓 = βˆ… ↔ 𝑀 = βˆ…))
7875, 77bitr3id 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (ran 𝑓 = βˆ… ↔ 𝑀 = βˆ…))
7978necon3bid 2977 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (ran 𝑓 β‰  βˆ… ↔ 𝑀 β‰  βˆ…))
8079biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 β‰  βˆ…)
81 ordunifi 9289 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran 𝑓 βŠ† On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ ran 𝑓)
8266, 74, 80, 81syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ ran 𝑓)
8362, 82sseldd 3975 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ 𝑦)
8456, 58, 83rspcdva 3605 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ (πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴)
85 simp-4l 780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ πœ‘)
8627ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑦 ∈ On)
8786, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑦 βŠ† On)
88 ffvelcdm 7073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀) β†’ (π‘“β€˜π‘’) ∈ 𝑦)
8988adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ 𝑦)
9087, 89sseldd 3975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ On)
9161ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ ran 𝑓 βŠ† 𝑦)
9291, 87sstrd 3984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ ran 𝑓 βŠ† On)
93 vex 3470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑓 ∈ V
9493rnex 7896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran 𝑓 ∈ V
9594ssonunii 7761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ran 𝑓 βŠ† On β†’ βˆͺ ran 𝑓 ∈ On)
9692, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ βˆͺ ran 𝑓 ∈ On)
9769ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑓 Fn 𝑀)
98 simprr 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑒 ∈ 𝑀)
99 fnfvelrn 7072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 Fn 𝑀 ∧ 𝑒 ∈ 𝑀) β†’ (π‘“β€˜π‘’) ∈ ran 𝑓)
10097, 98, 99syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ ran 𝑓)
101 elssuni 4931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((π‘“β€˜π‘’) ∈ ran 𝑓 β†’ (π‘“β€˜π‘’) βŠ† βˆͺ ran 𝑓)
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) βŠ† βˆͺ ran 𝑓)
10328, 29, 30, 31ttukeylem5 10504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ ((π‘“β€˜π‘’) ∈ On ∧ βˆͺ ran 𝑓 ∈ On ∧ (π‘“β€˜π‘’) βŠ† βˆͺ ran 𝑓)) β†’ (πΊβ€˜(π‘“β€˜π‘’)) βŠ† (πΊβ€˜βˆͺ ran 𝑓))
10485, 90, 96, 102, 103syl13anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (πΊβ€˜(π‘“β€˜π‘’)) βŠ† (πΊβ€˜βˆͺ ran 𝑓))
105104sseld 3973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
106105anassrs 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ 𝑓:π‘€βŸΆπ‘¦) ∧ 𝑒 ∈ 𝑀) β†’ (𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
107106ralimdva 3159 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ 𝑓:π‘€βŸΆπ‘¦) β†’ (βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
108107expimpd 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ ((𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
109108impr 454 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
110109adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
111 dfss3 3962 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓) ↔ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
112110, 111sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓))
11328, 29, 30ttukeylem2 10501 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ ((πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴 ∧ 𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓))) β†’ 𝑀 ∈ 𝐴)
11454, 84, 112, 113syl12anc 834 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 ∈ 𝐴)
115 0ss 4388 . . . . . . . . . . . . . . . . . . . . . . . . 25 βˆ… βŠ† 𝐡
11628, 29, 30ttukeylem2 10501 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝐡 ∈ 𝐴 ∧ βˆ… βŠ† 𝐡)) β†’ βˆ… ∈ 𝐴)
117115, 116mpanr2 701 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝐡 ∈ 𝐴) β†’ βˆ… ∈ 𝐴)
11829, 117mpdan 684 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆ… ∈ 𝐴)
119118ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ βˆ… ∈ 𝐴)
12053, 114, 119pm2.61ne 3019 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑀 ∈ 𝐴)
121120expr 456 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ ((𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ 𝑀 ∈ 𝐴))
122121exlimdv 1928 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ 𝑀 ∈ 𝐴))
12352, 122mpd 15 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ 𝐴)
124123ex 412 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) β†’ 𝑀 ∈ 𝐴))
125124ssrdv 3980 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴)
12628, 29, 30ttukeylem1 10500 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴 ↔ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴))
127126ad2antrr 723 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴 ↔ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴))
128125, 127mpbird 257 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴)
129128adantr 480 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ Β¬ 𝑦 = βˆ…) β†’ βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴)
13034, 129ifclda 4555 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)) ∈ 𝐴)
131 uneq2 4149 . . . . . . . . . . . . . . 15 ({(πΉβ€˜βˆͺ 𝑦)} = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
132131eleq1d 2810 . . . . . . . . . . . . . 14 ({(πΉβ€˜βˆͺ 𝑦)} = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ (((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴))
133 un0 4382 . . . . . . . . . . . . . . . 16 ((πΊβ€˜βˆͺ 𝑦) βˆͺ βˆ…) = (πΊβ€˜βˆͺ 𝑦)
134 uneq2 4149 . . . . . . . . . . . . . . . 16 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ βˆ…) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
135133, 134eqtr3id 2778 . . . . . . . . . . . . . . 15 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ (πΊβ€˜βˆͺ 𝑦) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
136135eleq1d 2810 . . . . . . . . . . . . . 14 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴))
137 simpr 484 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) ∧ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴)
138 fveq2 6881 . . . . . . . . . . . . . . . . 17 (π‘Ž = βˆͺ 𝑦 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜βˆͺ 𝑦))
139138eleq1d 2810 . . . . . . . . . . . . . . . 16 (π‘Ž = βˆͺ 𝑦 β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴))
140 simplrr 775 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
141 vuniex 7722 . . . . . . . . . . . . . . . . . 18 βˆͺ 𝑦 ∈ V
142141sucid 6436 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑦 ∈ suc βˆͺ 𝑦
143 eloni 6364 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On β†’ Ord 𝑦)
144 orduniorsuc 7811 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑦 β†’ (𝑦 = βˆͺ 𝑦 ∨ 𝑦 = suc βˆͺ 𝑦))
14527, 143, 1443syl 18 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (𝑦 = βˆͺ 𝑦 ∨ 𝑦 = suc βˆͺ 𝑦))
146145orcanai 999 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ 𝑦 = suc βˆͺ 𝑦)
147142, 146eleqtrrid 2832 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ βˆͺ 𝑦 ∈ 𝑦)
148139, 140, 147rspcdva 3605 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴)
149148adantr 480 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) ∧ Β¬ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴) β†’ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴)
150132, 136, 137, 149ifbothda 4558 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴)
151130, 150ifclda 4555 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))) ∈ 𝐴)
15233, 151eqeltrd 2825 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)
153152expr 456 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴 β†’ (πΊβ€˜π‘¦) ∈ 𝐴))
15424, 153sylbird 260 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴) β†’ (πΊβ€˜π‘¦) ∈ 𝐴))
155154ex 412 . . . . . . . 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 7840 . . 3 (𝐢 ∈ On β†’ (πœ‘ β†’ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴)))
161160impd 410 . 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 395   ∨ wo 844  βˆ€wal 1531   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062  Vcvv 3466   βˆ– cdif 3937   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  ifcif 4520  π’« cpw 4594  {csn 4620  βˆͺ cuni 4899  βˆͺ ciun 4987   ↦ cmpt 5221  dom cdm 5666  ran crn 5667   β€œ cima 5669  Ord word 6353  Oncon0 6354  suc csuc 6356  Fun wfun 6527   Fn wfn 6528  βŸΆwf 6529  β€“ontoβ†’wfo 6531  β€“1-1-ontoβ†’wf1o 6532  β€˜cfv 6533  recscrecs 8365  Fincfn 8935  cardccrd 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-om 7849  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-1o 8461  df-er 8699  df-en 8936  df-dom 8937  df-fin 8939  df-card 9930
This theorem is referenced by:  ttukeylem7  10506
  Copyright terms: Public domain W3C validator