Metamath Proof Explorer

Theorem ttukeylem3

Description: Lemma for ttukey . (Contributed by Mario Carneiro, 11-May-2015)

Ref Expression
Hypotheses 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 ttukeylem3 ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐺 ‘ 𝐶 ) = if ( 𝐶 = ∪ 𝐶 , if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) , ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) ) )

Proof

Step Hyp Ref Expression
1 ttukeylem.1 ⊢ ( 𝜑 → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
2 ttukeylem.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3 ttukeylem.3 ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) )
4 ttukeylem.4 ⊢ 𝐺 = recs ( ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) ) )
5 4 tfr2 ⊢ ( 𝐶 ∈ On → ( 𝐺 ‘ 𝐶 ) = ( ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) ) ‘ ( 𝐺 ↾ 𝐶 ) ) )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐺 ‘ 𝐶 ) = ( ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) ) ‘ ( 𝐺 ↾ 𝐶 ) ) )
7 eqidd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 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 𝑧 ) } , ∅ ) ) ) ) )
8 simpr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → 𝑧 = ( 𝐺 ↾ 𝐶 ) )
9 8 dmeqd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → dom 𝑧 = dom ( 𝐺 ↾ 𝐶 ) )
10 4 tfr1 ⊢ 𝐺 Fn On
11 onss ⊢ ( 𝐶 ∈ On → 𝐶 ⊆ On )
12 11 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → 𝐶 ⊆ On )
13 fnssres ⊢ ( ( 𝐺 Fn On ∧ 𝐶 ⊆ On ) → ( 𝐺 ↾ 𝐶 ) Fn 𝐶 )
14 10 12 13 sylancr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ( 𝐺 ↾ 𝐶 ) Fn 𝐶 )
15 14 fndmd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → dom ( 𝐺 ↾ 𝐶 ) = 𝐶 )
16 9 15 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → dom 𝑧 = 𝐶 )
17 16 unieqd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ∪ dom 𝑧 = ∪ 𝐶 )
18 16 17 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ( dom 𝑧 = ∪ dom 𝑧 ↔ 𝐶 = ∪ 𝐶 ) )
19 16 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ( dom 𝑧 = ∅ ↔ 𝐶 = ∅ ) )
20 8 rneqd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ran 𝑧 = ran ( 𝐺 ↾ 𝐶 ) )
21 df-ima ⊢ ( 𝐺 “ 𝐶 ) = ran ( 𝐺 ↾ 𝐶 )
22 20 21 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ran 𝑧 = ( 𝐺 “ 𝐶 ) )
23 22 unieqd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ∪ ran 𝑧 = ∪ ( 𝐺 “ 𝐶 ) )
24 19 23 ifbieq2d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) = if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) )
25 8 17 fveq12d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ( 𝑧 ‘ ∪ dom 𝑧 ) = ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) )
26 17 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ( 𝐹 ‘ ∪ dom 𝑧 ) = ( 𝐹 ‘ ∪ 𝐶 ) )
27 26 sneqd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → { ( 𝐹 ‘ ∪ dom 𝑧 ) } = { ( 𝐹 ‘ ∪ 𝐶 ) } )
28 25 27 uneq12d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) = ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) )
29 28 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 ↔ ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 ) )
30 eqidd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ∅ = ∅ )
31 29 27 30 ifbieq12d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) = if ( ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) )
32 25 31 uneq12d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) ) = ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ if ( ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) )
33 18 24 32 ifbieq12d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) = if ( 𝐶 = ∪ 𝐶 , if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) , ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ if ( ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) ) )
34 onuni ⊢ ( 𝐶 ∈ On → ∪ 𝐶 ∈ On )
35 34 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ∪ 𝐶 ∈ On )
36 sucidg ⊢ ( ∪ 𝐶 ∈ On → ∪ 𝐶 ∈ suc ∪ 𝐶 )
37 35 36 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ∪ 𝐶 ∈ suc ∪ 𝐶 )
38 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
39 38 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → Ord 𝐶 )
40 orduniorsuc ⊢ ( Ord 𝐶 → ( 𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶 ) )
41 39 40 syl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → ( 𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶 ) )
42 41 orcanai ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝐶 = suc ∪ 𝐶 )
43 37 42 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ∪ 𝐶 ∈ 𝐶 )
44 43 fvresd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) = ( 𝐺 ‘ ∪ 𝐶 ) )
45 44 uneq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) = ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) )
46 45 eleq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 ↔ ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 ) )
47 46 ifbid ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → if ( ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) = if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) )
48 44 47 uneq12d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ if ( ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) = ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) )
49 48 ifeq2da ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → if ( 𝐶 = ∪ 𝐶 , if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) , ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ if ( ( ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) ) = if ( 𝐶 = ∪ 𝐶 , if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) , ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) ) )
50 33 49 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑧 = ( 𝐺 ↾ 𝐶 ) ) → if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) = if ( 𝐶 = ∪ 𝐶 , if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) , ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) ) )
51 fnfun ⊢ ( 𝐺 Fn On → Fun 𝐺 )
52 10 51 ax-mp ⊢ Fun 𝐺
53 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ On ) → 𝐶 ∈ On )
54 resfunexg ⊢ ( ( Fun 𝐺 ∧ 𝐶 ∈ On ) → ( 𝐺 ↾ 𝐶 ) ∈ V )
55 52 53 54 sylancr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐺 ↾ 𝐶 ) ∈ V )
56 2 elexd ⊢ ( 𝜑 → 𝐵 ∈ V )
57 funimaexg ⊢ ( ( Fun 𝐺 ∧ 𝐶 ∈ On ) → ( 𝐺 “ 𝐶 ) ∈ V )
58 52 57 mpan ⊢ ( 𝐶 ∈ On → ( 𝐺 “ 𝐶 ) ∈ V )
59 58 uniexd ⊢ ( 𝐶 ∈ On → ∪ ( 𝐺 “ 𝐶 ) ∈ V )
60 ifcl ⊢ ( ( 𝐵 ∈ V ∧ ∪ ( 𝐺 “ 𝐶 ) ∈ V ) → if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) ∈ V )
61 56 59 60 syl2an ⊢ ( ( 𝜑 ∧ 𝐶 ∈ On ) → if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) ∈ V )
62 fvex ⊢ ( 𝐺 ‘ ∪ 𝐶 ) ∈ V
63 snex ⊢ { ( 𝐹 ‘ ∪ 𝐶 ) } ∈ V
64 0ex ⊢ ∅ ∈ V
65 63 64 ifex ⊢ if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ∈ V
66 62 65 unex ⊢ ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) ∈ V
67 ifcl ⊢ ( ( if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) ∈ V ∧ ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) ∈ V ) → if ( 𝐶 = ∪ 𝐶 , if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) , ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) ) ∈ V )
68 61 66 67 sylancl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ On ) → if ( 𝐶 = ∪ 𝐶 , if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) , ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) ) ∈ V )
69 7 50 55 68 fvmptd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) ) ‘ ( 𝐺 ↾ 𝐶 ) ) = if ( 𝐶 = ∪ 𝐶 , if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) , ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) ) )
70 6 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐺 ‘ 𝐶 ) = if ( 𝐶 = ∪ 𝐶 , if ( 𝐶 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝐶 ) ) , ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝐶 ) ∪ { ( 𝐹 ‘ ∪ 𝐶 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝐶 ) } , ∅ ) ) ) )