Metamath Proof Explorer


Theorem oieq2

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

Ref Expression
Assertion oieq2 ( 𝐴 = 𝐵 → OrdIso ( 𝑅 , 𝐴 ) = OrdIso ( 𝑅 , 𝐵 ) )

Proof

Step Hyp Ref Expression
1 weeq2 ( 𝐴 = 𝐵 → ( 𝑅 We 𝐴𝑅 We 𝐵 ) )
2 seeq2 ( 𝐴 = 𝐵 → ( 𝑅 Se 𝐴𝑅 Se 𝐵 ) )
3 1 2 anbi12d ( 𝐴 = 𝐵 → ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ↔ ( 𝑅 We 𝐵𝑅 Se 𝐵 ) ) )
4 rabeq ( 𝐴 = 𝐵 → { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } = { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } )
5 4 raleqdv ( 𝐴 = 𝐵 → ( ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ↔ ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) )
6 4 5 riotaeqbidv ( 𝐴 = 𝐵 → ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) = ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) )
7 6 mpteq2dv ( 𝐴 = 𝐵 → ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) = ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) )
8 recseq ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) = ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) → recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) = recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) )
9 7 8 syl ( 𝐴 = 𝐵 → recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) = recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) )
10 9 imaeq1d ( 𝐴 = 𝐵 → ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) = ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) )
11 10 raleqdv ( 𝐴 = 𝐵 → ( ∀ 𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 ↔ ∀ 𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 ) )
12 11 rexeqbi1dv ( 𝐴 = 𝐵 → ( ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 ↔ ∃ 𝑡𝐵𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 ) )
13 12 rabbidv ( 𝐴 = 𝐵 → { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } = { 𝑥 ∈ On ∣ ∃ 𝑡𝐵𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } )
14 9 13 reseq12d ( 𝐴 = 𝐵 → ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } ) = ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑥 ∈ On ∣ ∃ 𝑡𝐵𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } ) )
15 3 14 ifbieq1d ( 𝐴 = 𝐵 → if ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) , ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } ) , ∅ ) = if ( ( 𝑅 We 𝐵𝑅 Se 𝐵 ) , ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑥 ∈ On ∣ ∃ 𝑡𝐵𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } ) , ∅ ) )
16 df-oi OrdIso ( 𝑅 , 𝐴 ) = if ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) , ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } ) , ∅ )
17 df-oi OrdIso ( 𝑅 , 𝐵 ) = if ( ( 𝑅 We 𝐵𝑅 Se 𝐵 ) , ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑥 ∈ On ∣ ∃ 𝑡𝐵𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐵 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } ) , ∅ )
18 15 16 17 3eqtr4g ( 𝐴 = 𝐵 → OrdIso ( 𝑅 , 𝐴 ) = OrdIso ( 𝑅 , 𝐵 ) )