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