MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ttukeylem6 Structured version   Visualization version   GIF version
Theorem ttukeylem6 10511
Description: Lemma for ttukey 10515. (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 9941 . . . . 5 (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On
21onsuci 7824 . . . 4 suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On
32a1i 11 . . 3 (πœ‘ β†’ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On)
4 onelon 6383 . . 3 ((suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝐢 ∈ On)
53, 4sylan 579 . 2 ((πœ‘ ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝐢 ∈ On)
6 eleq1 2815 . . . . . 6 (𝑦 = π‘Ž β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ↔ π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))))
7 fveq2 6885 . . . . . . 7 (𝑦 = π‘Ž β†’ (πΊβ€˜π‘¦) = (πΊβ€˜π‘Ž))
87eleq1d 2812 . . . . . 6 (𝑦 = π‘Ž β†’ ((πΊβ€˜π‘¦) ∈ 𝐴 ↔ (πΊβ€˜π‘Ž) ∈ 𝐴))
96, 8imbi12d 344 . . . . 5 (𝑦 = π‘Ž β†’ ((𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴) ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
109imbi2d 340 . . . 4 (𝑦 = π‘Ž β†’ ((πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)) ↔ (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴))))
11 eleq1 2815 . . . . . 6 (𝑦 = 𝐢 β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ↔ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))))
12 fveq2 6885 . . . . . . 7 (𝑦 = 𝐢 β†’ (πΊβ€˜π‘¦) = (πΊβ€˜πΆ))
1312eleq1d 2812 . . . . . 6 (𝑦 = 𝐢 β†’ ((πΊβ€˜π‘¦) ∈ 𝐴 ↔ (πΊβ€˜πΆ) ∈ 𝐴))
1411, 13imbi12d 344 . . . . 5 (𝑦 = 𝐢 β†’ ((𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴) ↔ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴)))
1514imbi2d 340 . . . 4 (𝑦 = 𝐢 β†’ ((πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)) ↔ (πœ‘ β†’ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴))))
16 r19.21v 3173 . . . . . 6 (βˆ€π‘Ž ∈ 𝑦 (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)) ↔ (πœ‘ β†’ βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
172onordi 6469 . . . . . . . . . . . . . . 15 Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))
1817a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
19 ordelss 6374 . . . . . . . . . . . . . 14 ((Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝑦 βŠ† suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2018, 19sylan 579 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝑦 βŠ† suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2120sselda 3977 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) ∧ π‘Ž ∈ 𝑦) β†’ π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
22 biimt 360 . . . . . . . . . . . 12 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
2321, 22syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) ∧ π‘Ž ∈ 𝑦) β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
2423ralbidva 3169 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴 ↔ βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
252onssi 7823 . . . . . . . . . . . . . 14 suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) βŠ† On
26 simprl 768 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2725, 26sselid 3975 . . . . . . . . . . . . 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 10508 . . . . . . . . . . . . 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 4194 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ Fin)
3735elin1d 4193 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ 𝒫 βˆͺ (𝐺 β€œ 𝑦))
3837elpwid 4606 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 βŠ† βˆͺ (𝐺 β€œ 𝑦))
3931tfr1 8398 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 Fn On
40 fnfun 6643 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn On β†’ Fun 𝐺)
41 funiunfv 7243 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐺 β†’ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) = βˆͺ (𝐺 β€œ 𝑦))
4239, 40, 41mp2b 10 . . . . . . . . . . . . . . . . . . . . . 22 βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) = βˆͺ (𝐺 β€œ 𝑦)
4338, 42sseqtrrdi 4028 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£))
44 dfss3 3965 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£))
45 eliun 4994 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4645ralbii 3087 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘’ ∈ 𝑀 𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4744, 46bitri 275 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4843, 47sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
49 fveq2 6885 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (π‘“β€˜π‘’) β†’ (πΊβ€˜π‘£) = (πΊβ€˜(π‘“β€˜π‘’)))
5049eleq2d 2813 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (π‘“β€˜π‘’) β†’ (𝑒 ∈ (πΊβ€˜π‘£) ↔ 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
5150ac6sfi 9289 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ Fin ∧ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£)) β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
5236, 48, 51syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
53 eleq1 2815 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 = βˆ… β†’ (𝑀 ∈ 𝐴 ↔ βˆ… ∈ 𝐴))
54 simp-4l 780 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ πœ‘)
55 fveq2 6885 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž = βˆͺ ran 𝑓 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜βˆͺ ran 𝑓))
5655eleq1d 2812 . . . . . . . . . . . . . . . . . . . . . . . 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 6718 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:π‘€βŸΆπ‘¦ β†’ ran 𝑓 βŠ† 𝑦)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 βŠ† 𝑦)
6327ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑦 ∈ On)
64 onss 7769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ On β†’ 𝑦 βŠ† On)
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑦 βŠ† On)
6662, 65sstrd 3987 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 βŠ† On)
6736adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑀 ∈ Fin)
6867adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 ∈ Fin)
69 ffn 6711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:π‘€βŸΆπ‘¦ β†’ 𝑓 Fn 𝑀)
7060, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓 Fn 𝑀)
71 dffn4 6805 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 Fn 𝑀 ↔ 𝑓:𝑀–ontoβ†’ran 𝑓)
7270, 71sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓:𝑀–ontoβ†’ran 𝑓)
73 fofi 9340 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑀 ∈ Fin ∧ 𝑓:𝑀–ontoβ†’ran 𝑓) β†’ ran 𝑓 ∈ Fin)
7468, 72, 73syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 ∈ Fin)
75 dm0rn0 5918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑓 = βˆ… ↔ ran 𝑓 = βˆ…)
7659fdmd 6722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ dom 𝑓 = 𝑀)
7776eqeq1d 2728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (dom 𝑓 = βˆ… ↔ 𝑀 = βˆ…))
7875, 77bitr3id 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (ran 𝑓 = βˆ… ↔ 𝑀 = βˆ…))
7978necon3bid 2979 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (ran 𝑓 β‰  βˆ… ↔ 𝑀 β‰  βˆ…))
8079biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 β‰  βˆ…)
81 ordunifi 9295 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran 𝑓 βŠ† On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ ran 𝑓)
8266, 74, 80, 81syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ ran 𝑓)
8362, 82sseldd 3978 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ 𝑦)
8456, 58, 83rspcdva 3607 . . . . . . . . . . . . . . . . . . . . . . 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 7077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀) β†’ (π‘“β€˜π‘’) ∈ 𝑦)
8988adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ 𝑦)
9087, 89sseldd 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ On)
9161ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ ran 𝑓 βŠ† 𝑦)
9291, 87sstrd 3987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ ran 𝑓 βŠ† On)
93 vex 3472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑓 ∈ V
9493rnex 7900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran 𝑓 ∈ V
9594ssonunii 7765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 Fn 𝑀 ∧ 𝑒 ∈ 𝑀) β†’ (π‘“β€˜π‘’) ∈ ran 𝑓)
10097, 98, 99syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ ran 𝑓)
101 elssuni 4934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((π‘“β€˜π‘’) ∈ ran 𝑓 β†’ (π‘“β€˜π‘’) βŠ† βˆͺ ran 𝑓)
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) βŠ† βˆͺ ran 𝑓)
10328, 29, 30, 31ttukeylem5 10510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ ((π‘“β€˜π‘’) ∈ On ∧ βˆͺ ran 𝑓 ∈ On ∧ (π‘“β€˜π‘’) βŠ† βˆͺ ran 𝑓)) β†’ (πΊβ€˜(π‘“β€˜π‘’)) βŠ† (πΊβ€˜βˆͺ ran 𝑓))
10485, 90, 96, 102, 103syl13anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (πΊβ€˜(π‘“β€˜π‘’)) βŠ† (πΊβ€˜βˆͺ ran 𝑓))
105104sseld 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
106105anassrs 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ 𝑓:π‘€βŸΆπ‘¦) ∧ 𝑒 ∈ 𝑀) β†’ (𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
107106ralimdva 3161 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3965 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓) ↔ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
112110, 111sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓))
11328, 29, 30ttukeylem2 10507 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ ((πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴 ∧ 𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓))) β†’ 𝑀 ∈ 𝐴)
11454, 84, 112, 113syl12anc 834 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 ∈ 𝐴)
115 0ss 4391 . . . . . . . . . . . . . . . . . . . . . . . . 25 βˆ… βŠ† 𝐡
11628, 29, 30ttukeylem2 10507 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝐡 ∈ 𝐴 ∧ βˆ… βŠ† 𝐡)) β†’ βˆ… ∈ 𝐴)
117115, 116mpanr2 701 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝐡 ∈ 𝐴) β†’ βˆ… ∈ 𝐴)
11829, 117mpdan 684 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆ… ∈ 𝐴)
119118ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ βˆ… ∈ 𝐴)
12053, 114, 119pm2.61ne 3021 . . . . . . . . . . . . . . . . . . . . 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 3983 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴)
12628, 29, 30ttukeylem1 10506 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴 ↔ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴))
127126ad2antrr 723 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴 ↔ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴))
128125, 127mpbird 257 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴)
129128adantr 480 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ Β¬ 𝑦 = βˆ…) β†’ βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴)
13034, 129ifclda 4558 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)) ∈ 𝐴)
131 uneq2 4152 . . . . . . . . . . . . . . 15 ({(πΉβ€˜βˆͺ 𝑦)} = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
132131eleq1d 2812 . . . . . . . . . . . . . 14 ({(πΉβ€˜βˆͺ 𝑦)} = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ (((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴))
133 un0 4385 . . . . . . . . . . . . . . . 16 ((πΊβ€˜βˆͺ 𝑦) βˆͺ βˆ…) = (πΊβ€˜βˆͺ 𝑦)
134 uneq2 4152 . . . . . . . . . . . . . . . 16 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ βˆ…) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
135133, 134eqtr3id 2780 . . . . . . . . . . . . . . 15 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ (πΊβ€˜βˆͺ 𝑦) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
136135eleq1d 2812 . . . . . . . . . . . . . 14 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴))
137 simpr 484 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) ∧ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴)
138 fveq2 6885 . . . . . . . . . . . . . . . . 17 (π‘Ž = βˆͺ 𝑦 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜βˆͺ 𝑦))
139138eleq1d 2812 . . . . . . . . . . . . . . . 16 (π‘Ž = βˆͺ 𝑦 β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴))
140 simplrr 775 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
141 vuniex 7726 . . . . . . . . . . . . . . . . . 18 βˆͺ 𝑦 ∈ V
142141sucid 6440 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑦 ∈ suc βˆͺ 𝑦
143 eloni 6368 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On β†’ Ord 𝑦)
144 orduniorsuc 7815 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑦 β†’ (𝑦 = βˆͺ 𝑦 ∨ 𝑦 = suc βˆͺ 𝑦))
14527, 143, 1443syl 18 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (𝑦 = βˆͺ 𝑦 ∨ 𝑦 = suc βˆͺ 𝑦))
146145orcanai 999 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ 𝑦 = suc βˆͺ 𝑦)
147142, 146eleqtrrid 2834 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ βˆͺ 𝑦 ∈ 𝑦)
148139, 140, 147rspcdva 3607 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴)
149148adantr 480 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) ∧ Β¬ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴) β†’ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴)
150132, 136, 137, 149ifbothda 4561 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴)
151130, 150ifclda 4558 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))) ∈ 𝐴)
15233, 151eqeltrd 2827 . . . . . . . . . . 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 7844 . . 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 2934  βˆ€wral 3055  βˆƒwrex 3064  Vcvv 3468   βˆ– cdif 3940   βˆͺ cun 3941   ∩ cin 3942   βŠ† wss 3943  βˆ…c0 4317  ifcif 4523  π’« cpw 4597  {csn 4623  βˆͺ cuni 4902  βˆͺ ciun 4990   ↦ cmpt 5224  dom cdm 5669  ran crn 5670   β€œ cima 5672  Ord word 6357  Oncon0 6358  suc csuc 6360  Fun wfun 6531   Fn wfn 6532  βŸΆwf 6533  β€“ontoβ†’wfo 6535  β€“1-1-ontoβ†’wf1o 6536  β€˜cfv 6537  recscrecs 8371  Fincfn 8941  cardccrd 9932
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 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722
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 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7408  df-om 7853  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-1o 8467  df-er 8705  df-en 8942  df-dom 8943  df-fin 8945  df-card 9936
This theorem is referenced by:  ttukeylem7  10512
  Copyright terms: Public domain W3C validator