MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ttukeylem3 Structured version   Visualization version   GIF version
Theorem ttukeylem3 10509
Description: Lemma for ttukey 10516. (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 8401 . . 3 (𝐢 ∈ On β†’ (πΊβ€˜πΆ) = ((𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…))))β€˜(𝐺 β†Ύ 𝐢)))
32adantl 481 . 2 ((πœ‘ ∧ 𝐢 ∈ On) β†’ (πΊβ€˜πΆ) = ((𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…))))β€˜(𝐺 β†Ύ 𝐢)))
4 eqidd 2732 . . 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 484 . . . . . . . 8 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ 𝑧 = (𝐺 β†Ύ 𝐢))
65dmeqd 5906 . . . . . . 7 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ dom 𝑧 = dom (𝐺 β†Ύ 𝐢))
71tfr1 8400 . . . . . . . . 9 𝐺 Fn On
8 onss 7775 . . . . . . . . . 10 (𝐢 ∈ On β†’ 𝐢 βŠ† On)
98ad2antlr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ 𝐢 βŠ† On)
10 fnssres 6674 . . . . . . . . 9 ((𝐺 Fn On ∧ 𝐢 βŠ† On) β†’ (𝐺 β†Ύ 𝐢) Fn 𝐢)
117, 9, 10sylancr 586 . . . . . . . 8 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (𝐺 β†Ύ 𝐢) Fn 𝐢)
1211fndmd 6655 . . . . . . 7 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ dom (𝐺 β†Ύ 𝐢) = 𝐢)
136, 12eqtrd 2771 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ dom 𝑧 = 𝐢)
1413unieqd 4923 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ βˆͺ dom 𝑧 = βˆͺ 𝐢)
1513, 14eqeq12d 2747 . . . . 5 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (dom 𝑧 = βˆͺ dom 𝑧 ↔ 𝐢 = βˆͺ 𝐢))
1613eqeq1d 2733 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (dom 𝑧 = βˆ… ↔ 𝐢 = βˆ…))
175rneqd 5938 . . . . . . . 8 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ ran 𝑧 = ran (𝐺 β†Ύ 𝐢))
18 df-ima 5690 . . . . . . . 8 (𝐺 β€œ 𝐢) = ran (𝐺 β†Ύ 𝐢)
1917, 18eqtr4di 2789 . . . . . . 7 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ ran 𝑧 = (𝐺 β€œ 𝐢))
2019unieqd 4923 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ βˆͺ ran 𝑧 = βˆͺ (𝐺 β€œ 𝐢))
2116, 20ifbieq2d 4555 . . . . 5 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧) = if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)))
225, 14fveq12d 6899 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (π‘§β€˜βˆͺ dom 𝑧) = ((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢))
2314fveq2d 6896 . . . . . . . . . 10 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (πΉβ€˜βˆͺ dom 𝑧) = (πΉβ€˜βˆͺ 𝐢))
2423sneqd 4641 . . . . . . . . 9 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ {(πΉβ€˜βˆͺ dom 𝑧)} = {(πΉβ€˜βˆͺ 𝐢)})
2522, 24uneq12d 4165 . . . . . . . 8 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) = (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}))
2625eleq1d 2817 . . . . . . 7 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴 ↔ (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴))
27 eqidd 2732 . . . . . . 7 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ βˆ… = βˆ…)
2826, 24, 27ifbieq12d 4557 . . . . . 6 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…) = if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))
2922, 28uneq12d 4165 . . . . 5 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…)) = (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…)))
3015, 21, 29ifbieq12d 4557 . . . 4 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…))) = if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))))
31 onuni 7779 . . . . . . . . . 10 (𝐢 ∈ On β†’ βˆͺ 𝐢 ∈ On)
3231ad3antlr 728 . . . . . . . . 9 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ On)
33 sucidg 6446 . . . . . . . . 9 (βˆͺ 𝐢 ∈ On β†’ βˆͺ 𝐢 ∈ suc βˆͺ 𝐢)
3432, 33syl 17 . . . . . . . 8 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ suc βˆͺ 𝐢)
35 eloni 6375 . . . . . . . . . . 11 (𝐢 ∈ On β†’ Ord 𝐢)
3635ad2antlr 724 . . . . . . . . . 10 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ Ord 𝐢)
37 orduniorsuc 7821 . . . . . . . . . 10 (Ord 𝐢 β†’ (𝐢 = βˆͺ 𝐢 ∨ 𝐢 = suc βˆͺ 𝐢))
3836, 37syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ (𝐢 = βˆͺ 𝐢 ∨ 𝐢 = suc βˆͺ 𝐢))
3938orcanai 1000 . . . . . . . 8 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 = suc βˆͺ 𝐢)
4034, 39eleqtrrd 2835 . . . . . . 7 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ 𝐢)
4140fvresd 6912 . . . . . 6 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) = (πΊβ€˜βˆͺ 𝐢))
4241uneq1d 4163 . . . . . . . 8 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) = ((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}))
4342eleq1d 2817 . . . . . . 7 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴 ↔ ((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴))
4443ifbid 4552 . . . . . 6 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…) = if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))
4541, 44uneq12d 4165 . . . . 5 ((((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…)) = ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…)))
4645ifeq2da 4561 . . . 4 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), (((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ if((((𝐺 β†Ύ 𝐢)β€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))) = if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))))
4730, 46eqtrd 2771 . . 3 (((πœ‘ ∧ 𝐢 ∈ On) ∧ 𝑧 = (𝐺 β†Ύ 𝐢)) β†’ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…))) = if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))))
48 fnfun 6650 . . . . 5 (𝐺 Fn On β†’ Fun 𝐺)
497, 48ax-mp 5 . . . 4 Fun 𝐺
50 simpr 484 . . . 4 ((πœ‘ ∧ 𝐢 ∈ On) β†’ 𝐢 ∈ On)
51 resfunexg 7220 . . . 4 ((Fun 𝐺 ∧ 𝐢 ∈ On) β†’ (𝐺 β†Ύ 𝐢) ∈ V)
5249, 50, 51sylancr 586 . . 3 ((πœ‘ ∧ 𝐢 ∈ On) β†’ (𝐺 β†Ύ 𝐢) ∈ V)
53 ttukeylem.2 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ 𝐴)
5453elexd 3494 . . . . 5 (πœ‘ β†’ 𝐡 ∈ V)
55 funimaexg 6635 . . . . . . 7 ((Fun 𝐺 ∧ 𝐢 ∈ On) β†’ (𝐺 β€œ 𝐢) ∈ V)
5649, 55mpan 687 . . . . . 6 (𝐢 ∈ On β†’ (𝐺 β€œ 𝐢) ∈ V)
5756uniexd 7735 . . . . 5 (𝐢 ∈ On β†’ βˆͺ (𝐺 β€œ 𝐢) ∈ V)
58 ifcl 4574 . . . . 5 ((𝐡 ∈ V ∧ βˆͺ (𝐺 β€œ 𝐢) ∈ V) β†’ if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)) ∈ V)
5954, 57, 58syl2an 595 . . . 4 ((πœ‘ ∧ 𝐢 ∈ On) β†’ if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)) ∈ V)
60 fvex 6905 . . . . 5 (πΊβ€˜βˆͺ 𝐢) ∈ V
61 snex 5432 . . . . . 6 {(πΉβ€˜βˆͺ 𝐢)} ∈ V
62 0ex 5308 . . . . . 6 βˆ… ∈ V
6361, 62ifex 4579 . . . . 5 if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…) ∈ V
6460, 63unex 7736 . . . 4 ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…)) ∈ V
65 ifcl 4574 . . . 4 ((if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)) ∈ V ∧ ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…)) ∈ V) β†’ if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))) ∈ V)
6659, 64, 65sylancl 585 . . 3 ((πœ‘ ∧ 𝐢 ∈ On) β†’ if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))) ∈ V)
674, 47, 52, 66fvmptd 7006 . 2 ((πœ‘ ∧ 𝐢 ∈ On) β†’ ((𝑧 ∈ V ↦ if(dom 𝑧 = βˆͺ dom 𝑧, if(dom 𝑧 = βˆ…, 𝐡, βˆͺ ran 𝑧), ((π‘§β€˜βˆͺ dom 𝑧) βˆͺ if(((π‘§β€˜βˆͺ dom 𝑧) βˆͺ {(πΉβ€˜βˆͺ dom 𝑧)}) ∈ 𝐴, {(πΉβ€˜βˆͺ dom 𝑧)}, βˆ…))))β€˜(𝐺 β†Ύ 𝐢)) = if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))))
683, 67eqtrd 2771 1 ((πœ‘ ∧ 𝐢 ∈ On) β†’ (πΊβ€˜πΆ) = if(𝐢 = βˆͺ 𝐢, if(𝐢 = βˆ…, 𝐡, βˆͺ (𝐺 β€œ 𝐢)), ((πΊβ€˜βˆͺ 𝐢) βˆͺ if(((πΊβ€˜βˆͺ 𝐢) βˆͺ {(πΉβ€˜βˆͺ 𝐢)}) ∈ 𝐴, {(πΉβ€˜βˆͺ 𝐢)}, βˆ…))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844  βˆ€wal 1538   = wceq 1540   ∈ wcel 2105  Vcvv 3473   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  ifcif 4529  π’« cpw 4603  {csn 4629  βˆͺ cuni 4909   ↦ cmpt 5232  dom cdm 5677  ran crn 5678   β†Ύ cres 5679   β€œ cima 5680  Ord word 6364  Oncon0 6365  suc csuc 6367  Fun wfun 6538   Fn wfn 6539  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  recscrecs 8373  Fincfn 8942  cardccrd 9933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7415  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374
This theorem is referenced by:  ttukeylem4  10510  ttukeylem5  10511  ttukeylem6  10512  ttukeylem7  10513
  Copyright terms: Public domain W3C validator