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 7823 . . . 4 suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On
32a1i 11 . . 3 (πœ‘ β†’ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On)
4 onelon 6386 . . 3 ((suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∈ On ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝐢 ∈ On)
53, 4sylan 580 . 2 ((πœ‘ ∧ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝐢 ∈ On)
6 eleq1 2821 . . . . . 6 (𝑦 = π‘Ž β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ↔ π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))))
7 fveq2 6888 . . . . . . 7 (𝑦 = π‘Ž β†’ (πΊβ€˜π‘¦) = (πΊβ€˜π‘Ž))
87eleq1d 2818 . . . . . 6 (𝑦 = π‘Ž β†’ ((πΊβ€˜π‘¦) ∈ 𝐴 ↔ (πΊβ€˜π‘Ž) ∈ 𝐴))
96, 8imbi12d 344 . . . . 5 (𝑦 = π‘Ž β†’ ((𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴) ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
109imbi2d 340 . . . 4 (𝑦 = π‘Ž β†’ ((πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)) ↔ (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴))))
11 eleq1 2821 . . . . . 6 (𝑦 = 𝐢 β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ↔ 𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))))
12 fveq2 6888 . . . . . . 7 (𝑦 = 𝐢 β†’ (πΊβ€˜π‘¦) = (πΊβ€˜πΆ))
1312eleq1d 2818 . . . . . 6 (𝑦 = 𝐢 β†’ ((πΊβ€˜π‘¦) ∈ 𝐴 ↔ (πΊβ€˜πΆ) ∈ 𝐴))
1411, 13imbi12d 344 . . . . 5 (𝑦 = 𝐢 β†’ ((𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴) ↔ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴)))
1514imbi2d 340 . . . 4 (𝑦 = 𝐢 β†’ ((πœ‘ β†’ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)) ↔ (πœ‘ β†’ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴))))
16 r19.21v 3179 . . . . . 6 (βˆ€π‘Ž ∈ 𝑦 (πœ‘ β†’ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)) ↔ (πœ‘ β†’ βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
172onordi 6472 . . . . . . . . . . . . . . 15 Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))
1817a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
19 ordelss 6377 . . . . . . . . . . . . . 14 ((Ord suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝑦 βŠ† suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2018, 19sylan 580 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ 𝑦 βŠ† suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
2120sselda 3981 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) ∧ π‘Ž ∈ 𝑦) β†’ π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)))
22 biimt 360 . . . . . . . . . . . 12 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
2321, 22syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) ∧ π‘Ž ∈ 𝑦) β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
2423ralbidva 3175 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴 ↔ βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴)))
252onssi 7822 . . . . . . . . . . . . . 14 suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) βŠ† On
26 simprl 769 . . . . . . . . . . . . . 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 10502 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ On) β†’ (πΊβ€˜π‘¦) = if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))))
3327, 32syldan 591 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (πΊβ€˜π‘¦) = if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))))
3429ad3antrrr 728 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑦 = βˆ…) β†’ 𝐡 ∈ 𝐴)
35 simpr 485 . . . . . . . . . . . . . . . . . . . . 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 8393 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 Fn On
40 fnfun 6646 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn On β†’ Fun 𝐺)
41 funiunfv 7243 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐺 β†’ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) = βˆͺ (𝐺 β€œ 𝑦))
4239, 40, 41mp2b 10 . . . . . . . . . . . . . . . . . . . . . 22 βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) = βˆͺ (𝐺 β€œ 𝑦)
4338, 42sseqtrrdi 4032 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£))
44 dfss3 3969 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£))
45 eliun 5000 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4645ralbii 3093 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘’ ∈ 𝑀 𝑒 ∈ βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4744, 46bitri 274 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 βŠ† βˆͺ 𝑣 ∈ 𝑦 (πΊβ€˜π‘£) ↔ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
4843, 47sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£))
49 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (π‘“β€˜π‘’) β†’ (πΊβ€˜π‘£) = (πΊβ€˜(π‘“β€˜π‘’)))
5049eleq2d 2819 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (π‘“β€˜π‘’) β†’ (𝑒 ∈ (πΊβ€˜π‘£) ↔ 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
5150ac6sfi 9283 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ Fin ∧ βˆ€π‘’ ∈ 𝑀 βˆƒπ‘£ ∈ 𝑦 𝑒 ∈ (πΊβ€˜π‘£)) β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
5236, 48, 51syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))
53 eleq1 2821 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 = βˆ… β†’ (𝑀 ∈ 𝐴 ↔ βˆ… ∈ 𝐴))
54 simp-4l 781 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ πœ‘)
55 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž = βˆͺ ran 𝑓 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜βˆͺ ran 𝑓))
5655eleq1d 2818 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž = βˆͺ ran 𝑓 β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴))
57 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
5857ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
59 simprrl 779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑓:π‘€βŸΆπ‘¦)
6059adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓:π‘€βŸΆπ‘¦)
61 frn 6721 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:π‘€βŸΆπ‘¦ β†’ ran 𝑓 βŠ† 𝑦)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 βŠ† 𝑦)
6327ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑦 ∈ On)
64 onss 7768 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ On β†’ 𝑦 βŠ† On)
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑦 βŠ† On)
6662, 65sstrd 3991 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 βŠ† On)
6736adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑀 ∈ Fin)
6867adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 ∈ Fin)
69 ffn 6714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:π‘€βŸΆπ‘¦ β†’ 𝑓 Fn 𝑀)
7060, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑓 Fn 𝑀)
71 dffn4 6808 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 ∈ Fin)
75 dm0rn0 5922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑓 = βˆ… ↔ ran 𝑓 = βˆ…)
7659fdmd 6725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ dom 𝑓 = 𝑀)
7776eqeq1d 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (dom 𝑓 = βˆ… ↔ 𝑀 = βˆ…))
7875, 77bitr3id 284 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (ran 𝑓 = βˆ… ↔ 𝑀 = βˆ…))
7978necon3bid 2985 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ (ran 𝑓 β‰  βˆ… ↔ 𝑀 β‰  βˆ…))
8079biimpar 478 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ ran 𝑓 β‰  βˆ…)
81 ordunifi 9289 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran 𝑓 βŠ† On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ ran 𝑓)
8266, 74, 80, 81syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ ran 𝑓)
8362, 82sseldd 3982 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆͺ ran 𝑓 ∈ 𝑦)
8456, 58, 83rspcdva 3613 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ (πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴)
85 simp-4l 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ πœ‘)
8627ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑦 ∈ On)
8786, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑦 βŠ† On)
88 ffvelcdm 7080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀) β†’ (π‘“β€˜π‘’) ∈ 𝑦)
8988adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ 𝑦)
9087, 89sseldd 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ On)
9161ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ ran 𝑓 βŠ† 𝑦)
9291, 87sstrd 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ ran 𝑓 βŠ† On)
93 vex 3478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑓 ∈ V
9493rnex 7899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran 𝑓 ∈ V
9594ssonunii 7764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ran 𝑓 βŠ† On β†’ βˆͺ ran 𝑓 ∈ On)
9692, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ βˆͺ ran 𝑓 ∈ On)
9769ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑓 Fn 𝑀)
98 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ 𝑒 ∈ 𝑀)
99 fnfvelrn 7079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 Fn 𝑀 ∧ 𝑒 ∈ 𝑀) β†’ (π‘“β€˜π‘’) ∈ ran 𝑓)
10097, 98, 99syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (π‘“β€˜π‘’) ∈ ran 𝑓)
101 elssuni 4940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (πΊβ€˜(π‘“β€˜π‘’)) βŠ† (πΊβ€˜βˆͺ ran 𝑓))
105104sseld 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ 𝑒 ∈ 𝑀)) β†’ (𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
106105anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ 𝑓:π‘€βŸΆπ‘¦) ∧ 𝑒 ∈ 𝑀) β†’ (𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
107106ralimdva 3167 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) ∧ 𝑓:π‘€βŸΆπ‘¦) β†’ (βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’)) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
108107expimpd 454 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ ((𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓)))
109108impr 455 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
110109adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
111 dfss3 3969 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓) ↔ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜βˆͺ ran 𝑓))
112110, 111sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓))
11328, 29, 30ttukeylem2 10501 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ ((πΊβ€˜βˆͺ ran 𝑓) ∈ 𝐴 ∧ 𝑀 βŠ† (πΊβ€˜βˆͺ ran 𝑓))) β†’ 𝑀 ∈ 𝐴)
11454, 84, 112, 113syl12anc 835 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 ∈ 𝐴)
115 0ss 4395 . . . . . . . . . . . . . . . . . . . . . . . . 25 βˆ… βŠ† 𝐡
11628, 29, 30ttukeylem2 10501 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝐡 ∈ 𝐴 ∧ βˆ… βŠ† 𝐡)) β†’ βˆ… ∈ 𝐴)
117115, 116mpanr2 702 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝐡 ∈ 𝐴) β†’ βˆ… ∈ 𝐴)
11829, 117mpdan 685 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆ… ∈ 𝐴)
119118ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ βˆ… ∈ 𝐴)
12053, 114, 119pm2.61ne 3027 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) ∧ (𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))))) β†’ 𝑀 ∈ 𝐴)
121120expr 457 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ ((𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ 𝑀 ∈ 𝐴))
122121exlimdv 1936 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ‘¦ ∧ βˆ€π‘’ ∈ 𝑀 𝑒 ∈ (πΊβ€˜(π‘“β€˜π‘’))) β†’ 𝑀 ∈ 𝐴))
12352, 122mpd 15 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ 𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin)) β†’ 𝑀 ∈ 𝐴)
124123ex 413 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (𝑀 ∈ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) β†’ 𝑀 ∈ 𝐴))
125124ssrdv 3987 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴)
12628, 29, 30ttukeylem1 10500 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴 ↔ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴))
127126ad2antrr 724 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ (βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴 ↔ (𝒫 βˆͺ (𝐺 β€œ 𝑦) ∩ Fin) βŠ† 𝐴))
128125, 127mpbird 256 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴)
129128adantr 481 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) ∧ Β¬ 𝑦 = βˆ…) β†’ βˆͺ (𝐺 β€œ 𝑦) ∈ 𝐴)
13034, 129ifclda 4562 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ 𝑦 = βˆͺ 𝑦) β†’ if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)) ∈ 𝐴)
131 uneq2 4156 . . . . . . . . . . . . . . 15 ({(πΉβ€˜βˆͺ 𝑦)} = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
132131eleq1d 2818 . . . . . . . . . . . . . 14 ({(πΉβ€˜βˆͺ 𝑦)} = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ (((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴))
133 un0 4389 . . . . . . . . . . . . . . . 16 ((πΊβ€˜βˆͺ 𝑦) βˆͺ βˆ…) = (πΊβ€˜βˆͺ 𝑦)
134 uneq2 4156 . . . . . . . . . . . . . . . 16 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ βˆ…) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
135133, 134eqtr3id 2786 . . . . . . . . . . . . . . 15 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ (πΊβ€˜βˆͺ 𝑦) = ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)))
136135eleq1d 2818 . . . . . . . . . . . . . 14 (βˆ… = if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…) β†’ ((πΊβ€˜βˆͺ 𝑦) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴))
137 simpr 485 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) ∧ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴)
138 fveq2 6888 . . . . . . . . . . . . . . . . 17 (π‘Ž = βˆͺ 𝑦 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜βˆͺ 𝑦))
139138eleq1d 2818 . . . . . . . . . . . . . . . 16 (π‘Ž = βˆͺ 𝑦 β†’ ((πΊβ€˜π‘Ž) ∈ 𝐴 ↔ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴))
140 simplrr 776 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)
141 vuniex 7725 . . . . . . . . . . . . . . . . . 18 βˆͺ 𝑦 ∈ V
142141sucid 6443 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑦 ∈ suc βˆͺ 𝑦
143 eloni 6371 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On β†’ Ord 𝑦)
144 orduniorsuc 7814 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑦 β†’ (𝑦 = βˆͺ 𝑦 ∨ 𝑦 = suc βˆͺ 𝑦))
14527, 143, 1443syl 18 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (𝑦 = βˆͺ 𝑦 ∨ 𝑦 = suc βˆͺ 𝑦))
146145orcanai 1001 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ 𝑦 = suc βˆͺ 𝑦)
147142, 146eleqtrrid 2840 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ βˆͺ 𝑦 ∈ 𝑦)
148139, 140, 147rspcdva 3613 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴)
149148adantr 481 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) ∧ Β¬ ((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴) β†’ (πΊβ€˜βˆͺ 𝑦) ∈ 𝐴)
150132, 136, 137, 149ifbothda 4565 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) ∧ Β¬ 𝑦 = βˆͺ 𝑦) β†’ ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…)) ∈ 𝐴)
151130, 150ifclda 4562 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ if(𝑦 = βˆͺ 𝑦, if(𝑦 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝑦)), ((πΊβ€˜βˆͺ 𝑦) βˆͺ if(((πΊβ€˜βˆͺ 𝑦) βˆͺ {(πΉβ€˜βˆͺ 𝑦)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝑦)}, βˆ…))) ∈ 𝐴)
15233, 151eqeltrd 2833 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) ∧ βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴)) β†’ (πΊβ€˜π‘¦) ∈ 𝐴)
153152expr 457 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (πΊβ€˜π‘Ž) ∈ 𝐴 β†’ (πΊβ€˜π‘¦) ∈ 𝐴))
15424, 153sylbird 259 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡))) β†’ (βˆ€π‘Ž ∈ 𝑦 (π‘Ž ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜π‘Ž) ∈ 𝐴) β†’ (πΊβ€˜π‘¦) ∈ 𝐴))
155154ex 413 . . . . . . . 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 7843 . . 3 (𝐢 ∈ On β†’ (πœ‘ β†’ (𝐢 ∈ suc (cardβ€˜(βˆͺ 𝐴 βˆ– 𝐡)) β†’ (πΊβ€˜πΆ) ∈ 𝐴)))
161160impd 411 . 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 396   ∨ wo 845  βˆ€wal 1539   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   βˆ– 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 6360  Oncon0 6361  suc csuc 6363  Fun wfun 6534   Fn wfn 6535  βŸΆwf 6536  β€“ontoβ†’wfo 6538  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  recscrecs 8366  Fincfn 8935  cardccrd 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  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 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-1o 8462  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