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 ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ) )