MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac12lem1 Structured version   Visualization version   GIF version

Theorem dfac12lem1 9558
Description: Lemma for dfac12 9564. (Contributed by Mario Carneiro, 29-May-2015.)
Hypotheses
Ref Expression
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
Ref Expression
dfac12lem1 (𝜑 → (𝐺𝐶) = (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))))
Distinct variable groups:   𝑦,𝐴   𝑥,𝑦,𝐶   𝑥,𝐺,𝑦   𝜑,𝑦   𝑥,𝐹,𝑦   𝑦,𝐻
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)   𝐻(𝑥)

Proof of Theorem dfac12lem1
StepHypRef Expression
1 dfac12.5 . . 3 (𝜑𝐶 ∈ On)
2 dfac12.4 . . . 4 𝐺 = recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = dom 𝑥, ((suc ran ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((OrdIso( E , ran (𝑥 dom 𝑥)) ∘ (𝑥 dom 𝑥)) “ 𝑦))))))
32tfr2 8025 . . 3 (𝐶 ∈ On → (𝐺𝐶) = ((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = dom 𝑥, ((suc ran ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((OrdIso( E , ran (𝑥 dom 𝑥)) ∘ (𝑥 dom 𝑥)) “ 𝑦)))))‘(𝐺𝐶)))
41, 3syl 17 . 2 (𝜑 → (𝐺𝐶) = ((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = dom 𝑥, ((suc ran ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((OrdIso( E , ran (𝑥 dom 𝑥)) ∘ (𝑥 dom 𝑥)) “ 𝑦)))))‘(𝐺𝐶)))
52tfr1 8024 . . . . 5 𝐺 Fn On
6 fnfun 6450 . . . . 5 (𝐺 Fn On → Fun 𝐺)
75, 6ax-mp 5 . . . 4 Fun 𝐺
8 resfunexg 6973 . . . 4 ((Fun 𝐺𝐶 ∈ On) → (𝐺𝐶) ∈ V)
97, 1, 8sylancr 587 . . 3 (𝜑 → (𝐺𝐶) ∈ V)
10 dmeq 5771 . . . . . 6 (𝑥 = (𝐺𝐶) → dom 𝑥 = dom (𝐺𝐶))
1110fveq2d 6671 . . . . 5 (𝑥 = (𝐺𝐶) → (𝑅1‘dom 𝑥) = (𝑅1‘dom (𝐺𝐶)))
1210unieqd 4847 . . . . . . 7 (𝑥 = (𝐺𝐶) → dom 𝑥 = dom (𝐺𝐶))
1310, 12eqeq12d 2842 . . . . . 6 (𝑥 = (𝐺𝐶) → (dom 𝑥 = dom 𝑥 ↔ dom (𝐺𝐶) = dom (𝐺𝐶)))
14 rneq 5805 . . . . . . . . . . . . 13 (𝑥 = (𝐺𝐶) → ran 𝑥 = ran (𝐺𝐶))
15 df-ima 5567 . . . . . . . . . . . . 13 (𝐺𝐶) = ran (𝐺𝐶)
1614, 15syl6eqr 2879 . . . . . . . . . . . 12 (𝑥 = (𝐺𝐶) → ran 𝑥 = (𝐺𝐶))
1716unieqd 4847 . . . . . . . . . . 11 (𝑥 = (𝐺𝐶) → ran 𝑥 = (𝐺𝐶))
1817rneqd 5807 . . . . . . . . . 10 (𝑥 = (𝐺𝐶) → ran ran 𝑥 = ran (𝐺𝐶))
1918unieqd 4847 . . . . . . . . 9 (𝑥 = (𝐺𝐶) → ran ran 𝑥 = ran (𝐺𝐶))
20 suceq 6254 . . . . . . . . 9 ( ran ran 𝑥 = ran (𝐺𝐶) → suc ran ran 𝑥 = suc ran (𝐺𝐶))
2119, 20syl 17 . . . . . . . 8 (𝑥 = (𝐺𝐶) → suc ran ran 𝑥 = suc ran (𝐺𝐶))
2221oveq1d 7163 . . . . . . 7 (𝑥 = (𝐺𝐶) → (suc ran ran 𝑥 ·o (rank‘𝑦)) = (suc ran (𝐺𝐶) ·o (rank‘𝑦)))
23 fveq1 6666 . . . . . . . 8 (𝑥 = (𝐺𝐶) → (𝑥‘suc (rank‘𝑦)) = ((𝐺𝐶)‘suc (rank‘𝑦)))
2423fveq1d 6669 . . . . . . 7 (𝑥 = (𝐺𝐶) → ((𝑥‘suc (rank‘𝑦))‘𝑦) = (((𝐺𝐶)‘suc (rank‘𝑦))‘𝑦))
2522, 24oveq12d 7166 . . . . . 6 (𝑥 = (𝐺𝐶) → ((suc ran ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)) = ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o (((𝐺𝐶)‘suc (rank‘𝑦))‘𝑦)))
26 id 22 . . . . . . . . . . . . 13 (𝑥 = (𝐺𝐶) → 𝑥 = (𝐺𝐶))
2726, 12fveq12d 6674 . . . . . . . . . . . 12 (𝑥 = (𝐺𝐶) → (𝑥 dom 𝑥) = ((𝐺𝐶)‘ dom (𝐺𝐶)))
2827rneqd 5807 . . . . . . . . . . 11 (𝑥 = (𝐺𝐶) → ran (𝑥 dom 𝑥) = ran ((𝐺𝐶)‘ dom (𝐺𝐶)))
29 oieq2 8966 . . . . . . . . . . 11 (ran (𝑥 dom 𝑥) = ran ((𝐺𝐶)‘ dom (𝐺𝐶)) → OrdIso( E , ran (𝑥 dom 𝑥)) = OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))))
3028, 29syl 17 . . . . . . . . . 10 (𝑥 = (𝐺𝐶) → OrdIso( E , ran (𝑥 dom 𝑥)) = OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))))
3130cnveqd 5745 . . . . . . . . 9 (𝑥 = (𝐺𝐶) → OrdIso( E , ran (𝑥 dom 𝑥)) = OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))))
3231, 27coeq12d 5734 . . . . . . . 8 (𝑥 = (𝐺𝐶) → (OrdIso( E , ran (𝑥 dom 𝑥)) ∘ (𝑥 dom 𝑥)) = (OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) ∘ ((𝐺𝐶)‘ dom (𝐺𝐶))))
3332imaeq1d 5926 . . . . . . 7 (𝑥 = (𝐺𝐶) → ((OrdIso( E , ran (𝑥 dom 𝑥)) ∘ (𝑥 dom 𝑥)) “ 𝑦) = ((OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) ∘ ((𝐺𝐶)‘ dom (𝐺𝐶))) “ 𝑦))
3433fveq2d 6671 . . . . . 6 (𝑥 = (𝐺𝐶) → (𝐹‘((OrdIso( E , ran (𝑥 dom 𝑥)) ∘ (𝑥 dom 𝑥)) “ 𝑦)) = (𝐹‘((OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) ∘ ((𝐺𝐶)‘ dom (𝐺𝐶))) “ 𝑦)))
3513, 25, 34ifbieq12d 4497 . . . . 5 (𝑥 = (𝐺𝐶) → 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 (𝐺𝐶))) “ 𝑦))))
3611, 35mpteq12dv 5148 . . . 4 (𝑥 = (𝐺𝐶) → (𝑦 ∈ (𝑅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 (𝐺𝐶))) “ 𝑦)))))
37 eqid 2826 . . . 4 (𝑥 ∈ 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 𝑥)) “ 𝑦)))))
38 fvex 6680 . . . . 5 (𝑅1‘dom (𝐺𝐶)) ∈ V
3938mptex 6981 . . . 4 (𝑦 ∈ (𝑅1‘dom (𝐺𝐶)) ↦ if(dom (𝐺𝐶) = dom (𝐺𝐶), ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o (((𝐺𝐶)‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) ∘ ((𝐺𝐶)‘ dom (𝐺𝐶))) “ 𝑦)))) ∈ V
4036, 37, 39fvmpt 6765 . . 3 ((𝐺𝐶) ∈ 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 (𝐺𝐶))) “ 𝑦)))))
419, 40syl 17 . 2 (𝜑 → ((𝑥 ∈ 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 (𝐺𝐶))) “ 𝑦)))))
42 onss 7493 . . . . . . . 8 (𝐶 ∈ On → 𝐶 ⊆ On)
431, 42syl 17 . . . . . . 7 (𝜑𝐶 ⊆ On)
44 fnssres 6467 . . . . . . 7 ((𝐺 Fn On ∧ 𝐶 ⊆ On) → (𝐺𝐶) Fn 𝐶)
455, 43, 44sylancr 587 . . . . . 6 (𝜑 → (𝐺𝐶) Fn 𝐶)
46 fndm 6452 . . . . . 6 ((𝐺𝐶) Fn 𝐶 → dom (𝐺𝐶) = 𝐶)
4745, 46syl 17 . . . . 5 (𝜑 → dom (𝐺𝐶) = 𝐶)
4847fveq2d 6671 . . . 4 (𝜑 → (𝑅1‘dom (𝐺𝐶)) = (𝑅1𝐶))
4948mpteq1d 5152 . . 3 (𝜑 → (𝑦 ∈ (𝑅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 (𝐺𝐶))) “ 𝑦)))))
5047adantr 481 . . . . . . 7 ((𝜑𝑦 ∈ (𝑅1𝐶)) → dom (𝐺𝐶) = 𝐶)
5150unieqd 4847 . . . . . . 7 ((𝜑𝑦 ∈ (𝑅1𝐶)) → dom (𝐺𝐶) = 𝐶)
5250, 51eqeq12d 2842 . . . . . 6 ((𝜑𝑦 ∈ (𝑅1𝐶)) → (dom (𝐺𝐶) = dom (𝐺𝐶) ↔ 𝐶 = 𝐶))
5352ifbid 4492 . . . . 5 ((𝜑𝑦 ∈ (𝑅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 (𝐺𝐶))) “ 𝑦))))
54 rankr1ai 9216 . . . . . . . . . . . 12 (𝑦 ∈ (𝑅1𝐶) → (rank‘𝑦) ∈ 𝐶)
5554ad2antlr 723 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ 𝐶)
56 simpr 485 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝐶 = 𝐶)
5755, 56eleqtrd 2920 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ 𝐶)
58 eloni 6199 . . . . . . . . . . . 12 (𝐶 ∈ On → Ord 𝐶)
59 ordsucuniel 7527 . . . . . . . . . . . 12 (Ord 𝐶 → ((rank‘𝑦) ∈ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
601, 58, 593syl 18 . . . . . . . . . . 11 (𝜑 → ((rank‘𝑦) ∈ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
6160ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((rank‘𝑦) ∈ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
6257, 61mpbid 233 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → suc (rank‘𝑦) ∈ 𝐶)
6362fvresd 6687 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺𝐶)‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑦)))
6463fveq1d 6669 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (((𝐺𝐶)‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑦))
6564oveq2d 7164 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o (((𝐺𝐶)‘suc (rank‘𝑦))‘𝑦)) = ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)))
6665ifeq1da 4500 . . . . 5 ((𝜑𝑦 ∈ (𝑅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 (𝐺𝐶))) “ 𝑦))))
6751adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom (𝐺𝐶) = 𝐶)
6867fveq2d 6671 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ((𝐺𝐶)‘ dom (𝐺𝐶)) = ((𝐺𝐶)‘ 𝐶))
691ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ On)
70 uniexg 7457 . . . . . . . . . . . . . . . . 17 (𝐶 ∈ On → 𝐶 ∈ V)
71 sucidg 6267 . . . . . . . . . . . . . . . . 17 ( 𝐶 ∈ V → 𝐶 ∈ suc 𝐶)
7269, 70, 713syl 18 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ suc 𝐶)
731adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (𝑅1𝐶)) → 𝐶 ∈ On)
74 orduniorsuc 7533 . . . . . . . . . . . . . . . . . 18 (Ord 𝐶 → (𝐶 = 𝐶𝐶 = suc 𝐶))
7573, 58, 743syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (𝑅1𝐶)) → (𝐶 = 𝐶𝐶 = suc 𝐶))
7675orcanai 998 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 = suc 𝐶)
7772, 76eleqtrrd 2921 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐶)
7877fvresd 6687 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ((𝐺𝐶)‘ 𝐶) = (𝐺 𝐶))
7968, 78eqtrd 2861 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ((𝐺𝐶)‘ dom (𝐺𝐶)) = (𝐺 𝐶))
8079rneqd 5807 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran ((𝐺𝐶)‘ dom (𝐺𝐶)) = ran (𝐺 𝐶))
81 oieq2 8966 . . . . . . . . . . . 12 (ran ((𝐺𝐶)‘ dom (𝐺𝐶)) = ran (𝐺 𝐶) → OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) = OrdIso( E , ran (𝐺 𝐶)))
8280, 81syl 17 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) = OrdIso( E , ran (𝐺 𝐶)))
8382cnveqd 5745 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) = OrdIso( E , ran (𝐺 𝐶)))
8483, 79coeq12d 5734 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) ∘ ((𝐺𝐶)‘ dom (𝐺𝐶))) = (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)))
85 dfac12.h . . . . . . . . 9 𝐻 = (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶))
8684, 85syl6eqr 2879 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) ∘ ((𝐺𝐶)‘ dom (𝐺𝐶))) = 𝐻)
8786imaeq1d 5926 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ((OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) ∘ ((𝐺𝐶)‘ dom (𝐺𝐶))) “ 𝑦) = (𝐻𝑦))
8887fveq2d 6671 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐹‘((OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) ∘ ((𝐺𝐶)‘ dom (𝐺𝐶))) “ 𝑦)) = (𝐹‘(𝐻𝑦)))
8988ifeq2da 4501 . . . . 5 ((𝜑𝑦 ∈ (𝑅1𝐶)) → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) ∘ ((𝐺𝐶)‘ dom (𝐺𝐶))) “ 𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))))
9053, 66, 893eqtrd 2865 . . . 4 ((𝜑𝑦 ∈ (𝑅1𝐶)) → if(dom (𝐺𝐶) = dom (𝐺𝐶), ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o (((𝐺𝐶)‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((OrdIso( E , ran ((𝐺𝐶)‘ dom (𝐺𝐶))) ∘ ((𝐺𝐶)‘ dom (𝐺𝐶))) “ 𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))))
9190mpteq2dva 5158 . . 3 (𝜑 → (𝑦 ∈ (𝑅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‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))))
9249, 91eqtrd 2861 . 2 (𝜑 → (𝑦 ∈ (𝑅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‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))))
934, 41, 923eqtrd 2865 1 (𝜑 → (𝐺𝐶) = (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 843   = wceq 1530  wcel 2107  Vcvv 3500  wss 3940  ifcif 4470  𝒫 cpw 4542   cuni 4837  cmpt 5143   E cep 5463  ccnv 5553  dom cdm 5554  ran crn 5555  cres 5556  cima 5557  ccom 5558  Ord word 6188  Oncon0 6189  suc csuc 6191  Fun wfun 6346   Fn wfn 6347  1-1wf1 6349  cfv 6352  (class class class)co 7148  recscrecs 7998   +o coa 8090   ·o comu 8091  OrdIsocoi 8962  harchar 9009  𝑅1cr1 9180  rankcrnk 9181
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-riota 7106  df-ov 7151  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-oi 8963  df-r1 9182  df-rank 9183
This theorem is referenced by:  dfac12lem2  9559
  Copyright terms: Public domain W3C validator