Metamath Proof Explorer

Theorem oieq1

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

Ref Expression
Assertion oieq1 ⊢ R = S → OrdIso R A = OrdIso S A

Proof

Step Hyp Ref Expression
1 weeq1 ⊢ R = S → R We A ↔ S We A
2 seeq1 ⊢ R = S → R Se A ↔ S Se A
3 1 2 anbi12d ⊢ R = S → R We A ∧ R Se A ↔ S We A ∧ S Se A
4 breq ⊢ R = S → j R w ↔ j S w
5 4 ralbidv ⊢ R = S → ∀ j ∈ ran ⁡ h j R w ↔ ∀ j ∈ ran ⁡ h j S w
6 5 rabbidv ⊢ R = S → w ∈ A | ∀ j ∈ ran ⁡ h j R w = w ∈ A | ∀ j ∈ ran ⁡ h j S w
7 breq ⊢ R = S → u R v ↔ u S v
8 7 notbid ⊢ R = S → ¬ u R v ↔ ¬ u S v
9 6 8 raleqbidv ⊢ R = S → ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↔ ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v
10 6 9 riotaeqbidv ⊢ R = S → ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v = ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v
11 10 mpteq2dv ⊢ R = S → 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 ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v
12 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 ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S 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 ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v
13 11 12 syl ⊢ R = S → 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 ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v
14 13 imaeq1d ⊢ R = S → 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 ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v x
15 breq ⊢ R = S → z R t ↔ z S t
16 14 15 raleqbidv ⊢ R = S → ∀ 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 ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v x z S t
17 16 rexbidv ⊢ R = S → ∃ 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 ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v x z S t
18 17 rabbidv ⊢ R = S → 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 ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v x z S t
19 13 18 reseq12d ⊢ R = S → 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 ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v x z S t
20 3 19 ifbieq1d ⊢ R = S → 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 S We A ∧ S Se A recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v x z S t ∅
21 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 ∅
22 df-oi ⊢ OrdIso S A = if S We A ∧ S Se A recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j S w ¬ u S v x z S t ∅
23 20 21 22 3eqtr4g ⊢ R = S → OrdIso R A = OrdIso S A