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 7829 . . . 4 suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On
32a1i 11 . . 3 (πœ‘ β†’ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On)
4 onelon 6388 . . 3 ((suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝐢 ∈ On)
53, 4sylan 578 . 2 ((πœ‘ ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝐢 ∈ On)
6 eleq1 2819 . . . . . 6 (𝑦 = π‘Ž β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ↔ π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))))
7 fveq2 6890 . . . . . . 7 (𝑦 = π‘Ž β†’ (πΊβ€˜π‘¦) = (πΊβ€˜π‘Ž))
87eleq1d 2816 . . . . . 6 (𝑦 = π‘Ž β†’ ((πΊβ€˜π‘¦) ∈ 𝐴 ↔ (πΊβ€˜π‘Ž) ∈ 𝐴))
96, 8imbi12d 343 . . . . 5 (𝑦 = π‘Ž β†’ ((𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴) ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
109imbi2d 339 . . . 4 (𝑦 = π‘Ž β†’ ((πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)) ↔ (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴))))
11 eleq1 2819 . . . . . 6 (𝑦 = 𝐢 β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ↔ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))))
12 fveq2 6890 . . . . . . 7 (𝑦 = 𝐢 β†’ (πΊβ€˜π‘¦) = (πΊβ€˜πΆ))
1312eleq1d 2816 . . . . . 6 (𝑦 = 𝐢 β†’ ((πΊβ€˜π‘¦) ∈ 𝐴 ↔ (πΊβ€˜πΆ) ∈ 𝐴))
1411, 13imbi12d 343 . . . . 5 (𝑦 = 𝐢 β†’ ((𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴) ↔ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴)))
1514imbi2d 339 . . . 4 (𝑦 = 𝐢 β†’ ((πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)) ↔ (πœ‘ β†’ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴))))
16 r19.21v 3177 . . . . . 6 (βˆ€π‘Ž ∈ 𝑦 (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)) ↔ (πœ‘ β†’ βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
172onordi 6474 . . . . . . . . . . . . . . 15 Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))
1817a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
19 ordelss 6379 . . . . . . . . . . . . . 14 ((Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝑦 βŠ† suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2018, 19sylan 578 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝑦 βŠ† suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2120sselda 3981 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) ∧ π‘Ž ∈ 𝑦) β†’ π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
22 biimt 359 . . . . . . . . . . . 12 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
2321, 22syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) ∧ π‘Ž ∈ 𝑦) β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
2423ralbidva 3173 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴 ↔ βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
252onssi 7828 . . . . . . . . . . . . . 14 suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) βŠ† On
26 simprl 767 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2725, 26sselid 3979 . . . . . . . . . . . . 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 589 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (πΊβ€˜π‘¦) = if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))))
3429ad3antrrr 726 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑦 = βˆ…) β†’ 𝐡 ∈ 𝐴)
35 simpr 483 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin))
3635elin2d 4198 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ Fin)
3735elin1d 4197 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ 𝒫 βˆͺ (𝐺 β€œ 𝑦))
3837elpwid 4610 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 βŠ† βˆͺ (𝐺 β€œ 𝑦))
3931tfr1 8399 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 Fn On
40 fnfun 6648 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn On β†’ Fun 𝐺)
41 funiunfv 7249 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐺 β†’ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) = βˆͺ (𝐺 β€œ 𝑦))
4239, 40, 41mp2b 10 . . . . . . . . . . . . . . . . . . . . . 22 βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) = βˆͺ (𝐺 β€œ 𝑦)
4338, 42sseqtrrdi 4032 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£))
44 dfss3 3969 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£))
45 eliun 5000 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4645ralbii 3091 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘’ ∈ 𝑀 𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4744, 46bitri 274 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4843, 47sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
49 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (π‘“β€˜π‘’) β†’ (πΊβ€˜π‘£) = (πΊβ€˜(π‘“β€˜π‘’)))
5049eleq2d 2817 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (π‘“β€˜π‘’) β†’ (𝑒 ∈ (πΊβ€˜π‘£) ↔ 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
5150ac6sfi 9289 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ Fin ∧ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£)) β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
5236, 48, 51syl2anc 582 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
53 eleq1 2819 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 = βˆ… β†’ (𝑀 ∈ 𝐴 ↔ βˆ… ∈ 𝐴))
54 simp-4l 779 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ πœ‘)
55 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž = βˆͺ ran 𝑓 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜βˆͺ ran 𝑓))
5655eleq1d 2816 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž = βˆͺ ran 𝑓 β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴))
57 simplrr 774 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
5857ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
59 simprrl 777 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑓:π‘€βŸΆπ‘¦)
6059adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓:π‘€βŸΆπ‘¦)
61 frn 6723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:π‘€βŸΆπ‘¦ β†’ ran 𝑓 βŠ† 𝑦)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 βŠ† 𝑦)
6327ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑦 ∈ On)
64 onss 7774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ On β†’ 𝑦 βŠ† On)
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑦 βŠ† On)
6662, 65sstrd 3991 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 βŠ† On)
6736adantrr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑀 ∈ Fin)
6867adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 ∈ Fin)
69 ffn 6716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:π‘€βŸΆπ‘¦ β†’ 𝑓 Fn 𝑀)
7060, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓 Fn 𝑀)
71 dffn4 6810 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 ∈ Fin)
75 dm0rn0 5923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑓 = βˆ… ↔ ran 𝑓 = βˆ…)
7659fdmd 6727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ dom 𝑓 = 𝑀)
7776eqeq1d 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (dom 𝑓 = βˆ… ↔ 𝑀 = βˆ…))
7875, 77bitr3id 284 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (ran 𝑓 = βˆ… ↔ 𝑀 = βˆ…))
7978necon3bid 2983 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (ran 𝑓 β‰  βˆ… ↔ 𝑀 β‰  βˆ…))
8079biimpar 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 β‰  βˆ…)
81 ordunifi 9295 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran 𝑓 βŠ† On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ ran 𝑓)
8266, 74, 80, 81syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ ran 𝑓)
8362, 82sseldd 3982 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ 𝑦)
8456, 58, 83rspcdva 3612 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ (πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴)
85 simp-4l 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ πœ‘)
8627ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑦 ∈ On)
8786, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑦 βŠ† On)
88 ffvelcdm 7082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀) β†’ (π‘“β€˜π‘’) ∈ 𝑦)
8988adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ 𝑦)
9087, 89sseldd 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ On)
9161ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ ran 𝑓 βŠ† 𝑦)
9291, 87sstrd 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ ran 𝑓 βŠ† On)
93 vex 3476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑓 ∈ V
9493rnex 7905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran 𝑓 ∈ V
9594ssonunii 7770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ran 𝑓 βŠ† On β†’ βˆͺ ran 𝑓 ∈ On)
9692, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ βˆͺ ran 𝑓 ∈ On)
9769ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑓 Fn 𝑀)
98 simprr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑒 ∈ 𝑀)
99 fnfvelrn 7081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 Fn 𝑀 ∧ 𝑒 ∈ 𝑀) β†’ (π‘“β€˜π‘’) ∈ ran 𝑓)
10097, 98, 99syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ ran 𝑓)
101 elssuni 4940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (πΊβ€˜(π‘“β€˜π‘’)) βŠ† (πΊβ€˜βˆͺ ran 𝑓))
105104sseld 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
106105anassrs 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ 𝑓:π‘€βŸΆπ‘¦) ∧ 𝑒 ∈ 𝑀) β†’ (𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
107106ralimdva 3165 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ 𝑓:π‘€βŸΆπ‘¦) β†’ (βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
108107expimpd 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ ((𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
109108impr 453 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
110109adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
111 dfss3 3969 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓) ↔ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
112110, 111sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓))
11328, 29, 30ttukeylem2 10507 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ ((πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴 ∧ 𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓))) β†’ 𝑀 ∈ 𝐴)
11454, 84, 112, 113syl12anc 833 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 ∈ 𝐴)
115 0ss 4395 . . . . . . . . . . . . . . . . . . . . . . . . 25 βˆ… βŠ† 𝐡
11628, 29, 30ttukeylem2 10507 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝐡 ∈ 𝐴 ∧ βˆ… βŠ† 𝐡)) β†’ βˆ… ∈ 𝐴)
117115, 116mpanr2 700 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝐡 ∈ 𝐴) β†’ βˆ… ∈ 𝐴)
11829, 117mpdan 683 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆ… ∈ 𝐴)
119118ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ βˆ… ∈ 𝐴)
12053, 114, 119pm2.61ne 3025 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑀 ∈ 𝐴)
121120expr 455 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ ((𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ 𝑀 ∈ 𝐴))
122121exlimdv 1934 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ 𝑀 ∈ 𝐴))
12352, 122mpd 15 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ 𝐴)
124123ex 411 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) β†’ 𝑀 ∈ 𝐴))
125124ssrdv 3987 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴)
12628, 29, 30ttukeylem1 10506 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴 ↔ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴))
127126ad2antrr 722 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴 ↔ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴))
128125, 127mpbird 256 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴)
129128adantr 479 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ Β¬ 𝑦 = βˆ…) β†’ βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴)
13034, 129ifclda 4562 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)) ∈ 𝐴)
131 uneq2 4156 . . . . . . . . . . . . . . 15 ({(πΉβ€˜βˆͺ 𝑦)} = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
132131eleq1d 2816 . . . . . . . . . . . . . 14 ({(πΉβ€˜βˆͺ 𝑦)} = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ (((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴))
133 un0 4389 . . . . . . . . . . . . . . . 16 ((πΊβ€˜βˆͺ 𝑦) βˆͺ βˆ…) = (πΊβ€˜βˆͺ 𝑦)
134 uneq2 4156 . . . . . . . . . . . . . . . 16 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ βˆ…) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
135133, 134eqtr3id 2784 . . . . . . . . . . . . . . 15 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ (πΊβ€˜βˆͺ 𝑦) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
136135eleq1d 2816 . . . . . . . . . . . . . 14 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴))
137 simpr 483 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) ∧ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴)
138 fveq2 6890 . . . . . . . . . . . . . . . . 17 (π‘Ž = βˆͺ 𝑦 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜βˆͺ 𝑦))
139138eleq1d 2816 . . . . . . . . . . . . . . . 16 (π‘Ž = βˆͺ 𝑦 β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴))
140 simplrr 774 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
141 vuniex 7731 . . . . . . . . . . . . . . . . . 18 βˆͺ 𝑦 ∈ V
142141sucid 6445 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑦 ∈ suc βˆͺ 𝑦
143 eloni 6373 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On β†’ Ord 𝑦)
144 orduniorsuc 7820 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑦 β†’ (𝑦 = βˆͺ 𝑦 ∨ 𝑦 = suc βˆͺ 𝑦))
14527, 143, 1443syl 18 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (𝑦 = βˆͺ 𝑦 ∨ 𝑦 = suc βˆͺ 𝑦))
146145orcanai 999 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ 𝑦 = suc βˆͺ 𝑦)
147142, 146eleqtrrid 2838 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ βˆͺ 𝑦 ∈ 𝑦)
148139, 140, 147rspcdva 3612 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴)
149148adantr 479 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) ∧ Β¬ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴) β†’ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴)
150132, 136, 137, 149ifbothda 4565 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴)
151130, 150ifclda 4562 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))) ∈ 𝐴)
15233, 151eqeltrd 2831 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)
153152expr 455 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴 β†’ (πΊβ€˜π‘¦) ∈ 𝐴))
15424, 153sylbird 259 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴) β†’ (πΊβ€˜π‘¦) ∈ 𝐴))
155154ex 411 . . . . . . . 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 7849 . . 3 (𝐢 ∈ On β†’ (πœ‘ β†’ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴)))
161160impd 409 . 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 394   ∨ wo 843  βˆ€wal 1537   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  ifcif 4527  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907  βˆͺ ciun 4996   ↦ cmpt 5230  dom cdm 5675  ran crn 5676   β€œ cima 5678  Ord word 6362  Oncon0 6363  suc csuc 6365  Fun wfun 6536   Fn wfn 6537  βŸΆwf 6538  β€“ontoβ†’wfo 6540  β€“1-1-ontoβ†’wf1o 6541  β€˜cfv 6542  recscrecs 8372  Fincfn 8941  cardccrd 9932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-1o 8468  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