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 ( 𝑅 , 𝐵 ) ) |