MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ttukeylem3 Structured version   Visualization version   GIF version
Theorem ttukeylem3 10508
Description: Lemma for ttukey 10515. (Contributed by Mario Carneiro, 11-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
ttukeylem3 ((πœ‘ ∧ 𝐢 ∈ On) β†’ (πΊβ€˜πΆ) = if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))))
Distinct variable groups:   π‘₯,𝑧,𝐢   π‘₯,𝐺,𝑧   πœ‘,𝑧   π‘₯,𝐴,𝑧   π‘₯,𝐡,𝑧   π‘₯,𝐹,𝑧
Allowed substitution hint:   πœ‘(π‘₯)
Proof of Theorem ttukeylem3
StepHypRef Expression
1 ttukeylem.4 . . . 4 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…)))))
21tfr2 8400 . . 3 (𝐢 ∈ On β†’ (πΊβ€˜πΆ) = ((𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…))))β€˜(𝐺 β†Ύ 𝐢)))
32adantl 480 . 2 ((πœ‘ ∧ 𝐢 ∈ On) β†’ (πΊβ€˜πΆ) = ((𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…))))β€˜(𝐺 β†Ύ 𝐢)))
4 eqidd 2731 . . 3 ((πœ‘ ∧ 𝐢 ∈ On) β†’ (𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…)))) = (𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…)))))
5 simpr 483 . . . . . . . 8 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ 𝑧 = (𝐺 β†Ύ 𝐢))
65dmeqd 5904 . . . . . . 7 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ dom 𝑧 = dom (𝐺 β†Ύ 𝐢))
71tfr1 8399 . . . . . . . . 9 𝐺 Fn On
8 onss 7774 . . . . . . . . . 10 (𝐢 ∈ On β†’ 𝐢 βŠ† On)
98ad2antlr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ 𝐢 βŠ† On)
10 fnssres 6672 . . . . . . . . 9 ((𝐺 Fn On ∧ 𝐢 βŠ† On) β†’ (𝐺 β†Ύ 𝐢) Fn 𝐢)
117, 9, 10sylancr 585 . . . . . . . 8 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (𝐺 β†Ύ 𝐢) Fn 𝐢)
1211fndmd 6653 . . . . . . 7 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ dom (𝐺 β†Ύ 𝐢) = 𝐢)
136, 12eqtrd 2770 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ dom 𝑧 = 𝐢)
1413unieqd 4921 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ βˆͺ dom 𝑧 = βˆͺ 𝐢)
1513, 14eqeq12d 2746 . . . . 5 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (dom 𝑧 = βˆͺ dom 𝑧 ↔ 𝐢 = βˆͺ 𝐢))
1613eqeq1d 2732 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (dom 𝑧 = βˆ… ↔ 𝐢 = βˆ…))
175rneqd 5936 . . . . . . . 8 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ ran 𝑧 = ran (𝐺 β†Ύ 𝐢))
18 df-ima 5688 . . . . . . . 8 (𝐺 β€œ 𝐢) = ran (𝐺 β†Ύ 𝐢)
1917, 18eqtr4di 2788 . . . . . . 7 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ ran 𝑧 = (𝐺 β€œ 𝐢))
2019unieqd 4921 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ βˆͺ ran 𝑧 = βˆͺ (𝐺 β€œ 𝐢))
2116, 20ifbieq2d 4553 . . . . 5 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧) = if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)))
225, 14fveq12d 6897 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (π‘§β€˜βˆͺ dom 𝑧) = ((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢))
2314fveq2d 6894 . . . . . . . . . 10 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (πΉβ€˜βˆͺ dom 𝑧) = (πΉβ€˜βˆͺ 𝐢))
2423sneqd 4639 . . . . . . . . 9 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ {(πΉβ€˜βˆͺ dom 𝑧)} = {(πΉβ€˜βˆͺ 𝐢)})
2522, 24uneq12d 4163 . . . . . . . 8 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) = (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}))
2625eleq1d 2816 . . . . . . 7 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴 ↔ (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴))
27 eqidd 2731 . . . . . . 7 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ βˆ… = βˆ…)
2826, 24, 27ifbieq12d 4555 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…) = if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))
2922, 28uneq12d 4163 . . . . 5 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…)) = (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…)))
3015, 21, 29ifbieq12d 4555 . . . 4 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…))) = if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))))
31 onuni 7778 . . . . . . . . . 10 (𝐢 ∈ On β†’ βˆͺ 𝐢 ∈ On)
3231ad3antlr 727 . . . . . . . . 9 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ On)
33 sucidg 6444 . . . . . . . . 9 (βˆͺ 𝐢 ∈ On β†’ βˆͺ 𝐢 ∈ suc βˆͺ 𝐢)
3432, 33syl 17 . . . . . . . 8 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ suc βˆͺ 𝐢)
35 eloni 6373 . . . . . . . . . . 11 (𝐢 ∈ On β†’ Ord 𝐢)
3635ad2antlr 723 . . . . . . . . . 10 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ Ord 𝐢)
37 orduniorsuc 7820 . . . . . . . . . 10 (Ord 𝐢 β†’ (𝐢 = βˆͺ 𝐢 ∨ 𝐢 = suc βˆͺ 𝐢))
3836, 37syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (𝐢 = βˆͺ 𝐢 ∨ 𝐢 = suc βˆͺ 𝐢))
3938orcanai 999 . . . . . . . 8 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 = suc βˆͺ 𝐢)
4034, 39eleqtrrd 2834 . . . . . . 7 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ 𝐢)
4140fvresd 6910 . . . . . 6 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) = (πΊβ€˜βˆͺ 𝐢))
4241uneq1d 4161 . . . . . . . 8 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) = ((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}))
4342eleq1d 2816 . . . . . . 7 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴))
4443ifbid 4550 . . . . . 6 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…) = if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))
4541, 44uneq12d 4163 . . . . 5 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…)) = ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…)))
4645ifeq2da 4559 . . . 4 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))) = if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))))
4730, 46eqtrd 2770 . . 3 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…))) = if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))))
48 fnfun 6648 . . . . 5 (𝐺 Fn On β†’ Fun 𝐺)
497, 48ax-mp 5 . . . 4 Fun 𝐺
50 simpr 483 . . . 4 ((πœ‘ ∧ 𝐢 ∈ On) β†’ 𝐢 ∈ On)
51 resfunexg 7218 . . . 4 ((Fun 𝐺 ∧ 𝐢 ∈ On) β†’ (𝐺 β†Ύ 𝐢) ∈ V)
5249, 50, 51sylancr 585 . . 3 ((πœ‘ ∧ 𝐢 ∈ On) β†’ (𝐺 β†Ύ 𝐢) ∈ V)
53 ttukeylem.2 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ 𝐴)
5453elexd 3493 . . . . 5 (πœ‘ β†’ 𝐡 ∈ V)
55 funimaexg 6633 . . . . . . 7 ((Fun 𝐺 ∧ 𝐢 ∈ On) β†’ (𝐺 β€œ 𝐢) ∈ V)
5649, 55mpan 686 . . . . . 6 (𝐢 ∈ On β†’ (𝐺 β€œ 𝐢) ∈ V)
5756uniexd 7734 . . . . 5 (𝐢 ∈ On β†’ βˆͺ (𝐺 β€œ 𝐢) ∈ V)
58 ifcl 4572 . . . . 5 ((𝐡 ∈ V ∧ βˆͺ (𝐺 β€œ 𝐢) ∈ V) β†’ if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)) ∈ V)
5954, 57, 58syl2an 594 . . . 4 ((πœ‘ ∧ 𝐢 ∈ On) β†’ if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)) ∈ V)
60 fvex 6903 . . . . 5 (πΊβ€˜βˆͺ 𝐢) ∈ V
61 snex 5430 . . . . . 6 {(πΉβ€˜βˆͺ 𝐢)} ∈ V
62 0ex 5306 . . . . . 6 βˆ… ∈ V
6361, 62ifex 4577 . . . . 5 if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…) ∈ V
6460, 63unex 7735 . . . 4 ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…)) ∈ V
65 ifcl 4572 . . . 4 ((if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)) ∈ V ∧ ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…)) ∈ V) β†’ if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))) ∈ V)
6659, 64, 65sylancl 584 . . 3 ((πœ‘ ∧ 𝐢 ∈ On) β†’ if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))) ∈ V)
674, 47, 52, 66fvmptd 7004 . 2 ((πœ‘ ∧ 𝐢 ∈ On) β†’ ((𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…))))β€˜(𝐺 β†Ύ 𝐢)) = if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))))
683, 67eqtrd 2770 1 ((πœ‘ ∧ 𝐢 ∈ On) β†’ (πΊβ€˜πΆ) = if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843  βˆ€wal 1537   = wceq 1539   ∈ wcel 2104  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  ifcif 4527  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907   ↦ cmpt 5230  dom cdm 5675  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678  Ord word 6362  Oncon0 6363  suc csuc 6365  Fun wfun 6536   Fn wfn 6537  β€“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-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-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-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-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373
This theorem is referenced by:  ttukeylem4  10509  ttukeylem5  10510  ttukeylem6  10511  ttukeylem7  10512
  Copyright terms: Public domain W3C validator