Metamath Proof Explorer

Theorem dfac12lem1

Description: Lemma for dfac12 . (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Hypotheses dfac12.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
dfac12.3 ⊢ ( 𝜑 → 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) –1-1→ On )
dfac12.4 ⊢ 𝐺 = recs ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) )
dfac12.5 ⊢ ( 𝜑 → 𝐶 ∈ On )
dfac12.h ⊢ 𝐻 = ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∘ ( 𝐺 ‘ ∪ 𝐶 ) )
Assertion dfac12lem1 ( 𝜑 → ( 𝐺 ‘ 𝐶 ) = ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↦ if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfac12.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
2 dfac12.3 ⊢ ( 𝜑 → 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) –1-1→ On )
3 dfac12.4 ⊢ 𝐺 = recs ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) )
4 dfac12.5 ⊢ ( 𝜑 → 𝐶 ∈ On )
5 dfac12.h ⊢ 𝐻 = ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∘ ( 𝐺 ‘ ∪ 𝐶 ) )
6 3 tfr2 ⊢ ( 𝐶 ∈ On → ( 𝐺 ‘ 𝐶 ) = ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) ‘ ( 𝐺 ↾ 𝐶 ) ) )
7 4 6 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) = ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) ‘ ( 𝐺 ↾ 𝐶 ) ) )
8 3 tfr1 ⊢ 𝐺 Fn On
9 fnfun ⊢ ( 𝐺 Fn On → Fun 𝐺 )
10 8 9 ax-mp ⊢ Fun 𝐺
11 resfunexg ⊢ ( ( Fun 𝐺 ∧ 𝐶 ∈ On ) → ( 𝐺 ↾ 𝐶 ) ∈ V )
12 10 4 11 sylancr ⊢ ( 𝜑 → ( 𝐺 ↾ 𝐶 ) ∈ V )
13 dmeq ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → dom 𝑥 = dom ( 𝐺 ↾ 𝐶 ) )
14 13 fveq2d ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ( 𝑅1 ‘ dom 𝑥 ) = ( 𝑅1 ‘ dom ( 𝐺 ↾ 𝐶 ) ) )
15 13 unieqd ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ∪ dom 𝑥 = ∪ dom ( 𝐺 ↾ 𝐶 ) )
16 13 15 eqeq12d ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ( dom 𝑥 = ∪ dom 𝑥 ↔ dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) ) )
17 rneq ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ran 𝑥 = ran ( 𝐺 ↾ 𝐶 ) )
18 df-ima ⊢ ( 𝐺 “ 𝐶 ) = ran ( 𝐺 ↾ 𝐶 )
19 17 18 eqtr4di ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ran 𝑥 = ( 𝐺 “ 𝐶 ) )
20 19 unieqd ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ∪ ran 𝑥 = ∪ ( 𝐺 “ 𝐶 ) )
21 20 rneqd ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ran ∪ ran 𝑥 = ran ∪ ( 𝐺 “ 𝐶 ) )
22 21 unieqd ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ∪ ran ∪ ran 𝑥 = ∪ ran ∪ ( 𝐺 “ 𝐶 ) )
23 suceq ⊢ ( ∪ ran ∪ ran 𝑥 = ∪ ran ∪ ( 𝐺 “ 𝐶 ) → suc ∪ ran ∪ ran 𝑥 = suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) )
24 22 23 syl ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → suc ∪ ran ∪ ran 𝑥 = suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) )
25 24 oveq1d ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) = ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) )
26 fveq1 ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) = ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) )
27 26 fveq1d ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) )
28 25 27 oveq12d ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) = ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) )
29 id ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → 𝑥 = ( 𝐺 ↾ 𝐶 ) )
30 29 15 fveq12d ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ( 𝑥 ‘ ∪ dom 𝑥 ) = ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) )
31 30 rneqd ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ran ( 𝑥 ‘ ∪ dom 𝑥 ) = ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) )
32 oieq2 ⊢ ( ran ( 𝑥 ‘ ∪ dom 𝑥 ) = ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) → OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) = OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) )
33 31 32 syl ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) = OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) )
34 33 cnveqd ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) = ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) )
35 34 30 coeq12d ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) = ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) )
36 35 imaeq1d ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) = ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) )
37 36 fveq2d ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) = ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) )
38 16 28 37 ifbieq12d ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) = if ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) )
39 14 38 mpteq12dv ⊢ ( 𝑥 = ( 𝐺 ↾ 𝐶 ) → ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 𝑅1 ‘ dom ( 𝐺 ↾ 𝐶 ) ) ↦ if ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) ) )
40 eqid ⊢ ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) = ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) )
41 fvex ⊢ ( 𝑅1 ‘ dom ( 𝐺 ↾ 𝐶 ) ) ∈ V
42 41 mptex ⊢ ( 𝑦 ∈ ( 𝑅1 ‘ dom ( 𝐺 ↾ 𝐶 ) ) ↦ if ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) ) ∈ V
43 39 40 42 fvmpt ⊢ ( ( 𝐺 ↾ 𝐶 ) ∈ V → ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) ‘ ( 𝐺 ↾ 𝐶 ) ) = ( 𝑦 ∈ ( 𝑅1 ‘ dom ( 𝐺 ↾ 𝐶 ) ) ↦ if ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) ) )
44 12 43 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) ‘ ( 𝐺 ↾ 𝐶 ) ) = ( 𝑦 ∈ ( 𝑅1 ‘ dom ( 𝐺 ↾ 𝐶 ) ) ↦ if ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) ) )
45 onss ⊢ ( 𝐶 ∈ On → 𝐶 ⊆ On )
46 4 45 syl ⊢ ( 𝜑 → 𝐶 ⊆ On )
47 fnssres ⊢ ( ( 𝐺 Fn On ∧ 𝐶 ⊆ On ) → ( 𝐺 ↾ 𝐶 ) Fn 𝐶 )
48 8 46 47 sylancr ⊢ ( 𝜑 → ( 𝐺 ↾ 𝐶 ) Fn 𝐶 )
49 48 fndmd ⊢ ( 𝜑 → dom ( 𝐺 ↾ 𝐶 ) = 𝐶 )
50 49 fveq2d ⊢ ( 𝜑 → ( 𝑅1 ‘ dom ( 𝐺 ↾ 𝐶 ) ) = ( 𝑅1 ‘ 𝐶 ) )
51 50 mpteq1d ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑅1 ‘ dom ( 𝐺 ↾ 𝐶 ) ) ↦ if ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↦ if ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) ) )
52 49 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → dom ( 𝐺 ↾ 𝐶 ) = 𝐶 )
53 52 unieqd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → ∪ dom ( 𝐺 ↾ 𝐶 ) = ∪ 𝐶 )
54 52 53 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) ↔ 𝐶 = ∪ 𝐶 ) )
55 54 ifbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → if ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) )
56 rankr1ai ⊢ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) → ( rank ‘ 𝑦 ) ∈ 𝐶 )
57 56 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( rank ‘ 𝑦 ) ∈ 𝐶 )
58 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → 𝐶 = ∪ 𝐶 )
59 57 58 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( rank ‘ 𝑦 ) ∈ ∪ 𝐶 )
60 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
61 ordsucuniel ⊢ ( Ord 𝐶 → ( ( rank ‘ 𝑦 ) ∈ ∪ 𝐶 ↔ suc ( rank ‘ 𝑦 ) ∈ 𝐶 ) )
62 4 60 61 3syl ⊢ ( 𝜑 → ( ( rank ‘ 𝑦 ) ∈ ∪ 𝐶 ↔ suc ( rank ‘ 𝑦 ) ∈ 𝐶 ) )
63 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( rank ‘ 𝑦 ) ∈ ∪ 𝐶 ↔ suc ( rank ‘ 𝑦 ) ∈ 𝐶 ) )
64 59 63 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → suc ( rank ‘ 𝑦 ) ∈ 𝐶 )
65 64 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) = ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) )
66 65 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) )
67 66 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) = ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) )
68 67 ifeq1da ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) )
69 53 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ∪ dom ( 𝐺 ↾ 𝐶 ) = ∪ 𝐶 )
70 69 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) = ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) )
71 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝐶 ∈ On )
72 uniexg ⊢ ( 𝐶 ∈ On → ∪ 𝐶 ∈ V )
73 sucidg ⊢ ( ∪ 𝐶 ∈ V → ∪ 𝐶 ∈ suc ∪ 𝐶 )
74 71 72 73 3syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ∪ 𝐶 ∈ suc ∪ 𝐶 )
75 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → 𝐶 ∈ On )
76 orduniorsuc ⊢ ( Ord 𝐶 → ( 𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶 ) )
77 75 60 76 3syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → ( 𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶 ) )
78 77 orcanai ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝐶 = suc ∪ 𝐶 )
79 74 78 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ∪ 𝐶 ∈ 𝐶 )
80 79 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ 𝐶 ) = ( 𝐺 ‘ ∪ 𝐶 ) )
81 70 80 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) = ( 𝐺 ‘ ∪ 𝐶 ) )
82 81 rneqd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) = ran ( 𝐺 ‘ ∪ 𝐶 ) )
83 oieq2 ⊢ ( ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) = ran ( 𝐺 ‘ ∪ 𝐶 ) → OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) = OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) )
84 82 83 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) = OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) )
85 84 cnveqd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) = ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) )
86 85 81 coeq12d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) = ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∘ ( 𝐺 ‘ ∪ 𝐶 ) ) )
87 86 5 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) = 𝐻 )
88 87 imaeq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) = ( 𝐻 “ 𝑦 ) )
89 88 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) = ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) )
90 89 ifeq2da ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) )
91 55 68 90 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → if ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) )
92 91 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↦ if ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↦ if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ) )
93 51 92 eqtrd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑅1 ‘ dom ( 𝐺 ↾ 𝐶 ) ) ↦ if ( dom ( 𝐺 ↾ 𝐶 ) = ∪ dom ( 𝐺 ↾ 𝐶 ) , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( ( 𝐺 ↾ 𝐶 ) ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) ∘ ( ( 𝐺 ↾ 𝐶 ) ‘ ∪ dom ( 𝐺 ↾ 𝐶 ) ) ) “ 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↦ if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ) )
94 7 44 93 3eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) = ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↦ if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ) )