Metamath Proof Explorer

Theorem dfac12lem1

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

Ref Expression
Hypotheses dfac12.1 ⊢ φ → A ∈ On
dfac12.3 ⊢ φ → F : 𝒫 har ⁡ R1 ⁡ A ⟶ 1-1 On
dfac12.4 ⊢ G = recs ⁡ x ∈ V ⟼ y ∈ R1 ⁡ dom ⁡ x ⟼ if dom ⁡ x = ⋃ dom ⁡ x suc ⁡ ⋃ ran ⁡ ⋃ ran ⁡ x ⋅ 𝑜 rank ⁡ y + 𝑜 x ⁡ suc ⁡ rank ⁡ y ⁡ y F ⁡ OrdIso E ran ⁡ x ⁡ ⋃ dom ⁡ x -1 ∘ x ⁡ ⋃ dom ⁡ x y
dfac12.5 ⊢ φ → C ∈ On
dfac12.h ⊢ H = OrdIso E ran ⁡ G ⁡ ⋃ C -1 ∘ G ⁡ ⋃ C
Assertion dfac12lem1 ⊢ φ → G ⁡ C = y ∈ R1 ⁡ C ⟼ if C = ⋃ C suc ⁡ ⋃ ran ⁡ ⋃ G C ⋅ 𝑜 rank ⁡ y + 𝑜 G ⁡ suc ⁡ rank ⁡ y ⁡ y F ⁡ H y

Proof

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