Metamath Proof Explorer

Theorem oieq2

Description: Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015)

Ref Expression
Assertion oieq2 ⊢ A = B → OrdIso R A = OrdIso R B

Proof

Step Hyp Ref Expression
1 weeq2 ⊢ A = B → R We A ↔ R We B
2 seeq2 ⊢ A = B → R Se A ↔ R Se B
3 1 2 anbi12d ⊢ A = B → R We A ∧ R Se A ↔ R We B ∧ R Se B
4 rabeq ⊢ A = B → w ∈ A | ∀ j ∈ ran ⁡ h j R w = w ∈ B | ∀ j ∈ ran ⁡ h j R w
5 4 raleqdv ⊢ A = B → ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↔ ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v
6 4 5 riotaeqbidv ⊢ A = B → ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v = ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v
7 6 mpteq2dv ⊢ A = B → h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v = h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v
8 recseq ⊢ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v = h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v → recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v
9 7 8 syl ⊢ A = B → recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v
10 9 imaeq1d ⊢ A = B → recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v x
11 10 raleqdv ⊢ A = B → ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ↔ ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
12 11 rexeqbi1dv ⊢ A = B → ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ↔ ∃ t ∈ B ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
13 12 rabbidv ⊢ A = B → x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t = x ∈ On | ∃ t ∈ B ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
14 9 13 reseq12d ⊢ A = B → recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ B ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
15 3 14 ifbieq1d ⊢ A = B → if R We A ∧ R Se A recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ∅ = if R We B ∧ R Se B recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ B ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ∅
16 df-oi ⊢ OrdIso R A = if R We A ∧ R Se A recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ∅
17 df-oi ⊢ OrdIso R B = if R We B ∧ R Se B recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ B ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ B | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ∅
18 15 16 17 3eqtr4g ⊢ A = B → OrdIso R A = OrdIso R B