Step |
Hyp |
Ref |
Expression |
1 |
|
cantnfs.s |
⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 ) |
2 |
|
cantnfs.a |
⊢ ( 𝜑 → 𝐴 ∈ On ) |
3 |
|
cantnfs.b |
⊢ ( 𝜑 → 𝐵 ∈ On ) |
4 |
|
oemapval.t |
⊢ 𝑇 = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } |
5 |
1 2 3 4
|
cantnf |
⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) ) |
6 |
|
isof1o |
⊢ ( ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) → ( 𝐴 CNF 𝐵 ) : 𝑆 –1-1-onto→ ( 𝐴 ↑o 𝐵 ) ) |
7 |
|
f1orel |
⊢ ( ( 𝐴 CNF 𝐵 ) : 𝑆 –1-1-onto→ ( 𝐴 ↑o 𝐵 ) → Rel ( 𝐴 CNF 𝐵 ) ) |
8 |
5 6 7
|
3syl |
⊢ ( 𝜑 → Rel ( 𝐴 CNF 𝐵 ) ) |
9 |
|
dfrel2 |
⊢ ( Rel ( 𝐴 CNF 𝐵 ) ↔ ◡ ◡ ( 𝐴 CNF 𝐵 ) = ( 𝐴 CNF 𝐵 ) ) |
10 |
8 9
|
sylib |
⊢ ( 𝜑 → ◡ ◡ ( 𝐴 CNF 𝐵 ) = ( 𝐴 CNF 𝐵 ) ) |
11 |
|
oecl |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On ) |
12 |
2 3 11
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 ↑o 𝐵 ) ∈ On ) |
13 |
|
eloni |
⊢ ( ( 𝐴 ↑o 𝐵 ) ∈ On → Ord ( 𝐴 ↑o 𝐵 ) ) |
14 |
12 13
|
syl |
⊢ ( 𝜑 → Ord ( 𝐴 ↑o 𝐵 ) ) |
15 |
|
isocnv |
⊢ ( ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) → ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) ) |
16 |
5 15
|
syl |
⊢ ( 𝜑 → ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) ) |
17 |
1 2 3 4
|
oemapwe |
⊢ ( 𝜑 → ( 𝑇 We 𝑆 ∧ dom OrdIso ( 𝑇 , 𝑆 ) = ( 𝐴 ↑o 𝐵 ) ) ) |
18 |
17
|
simpld |
⊢ ( 𝜑 → 𝑇 We 𝑆 ) |
19 |
|
ovex |
⊢ ( 𝐴 CNF 𝐵 ) ∈ V |
20 |
19
|
dmex |
⊢ dom ( 𝐴 CNF 𝐵 ) ∈ V |
21 |
1 20
|
eqeltri |
⊢ 𝑆 ∈ V |
22 |
|
exse |
⊢ ( 𝑆 ∈ V → 𝑇 Se 𝑆 ) |
23 |
21 22
|
ax-mp |
⊢ 𝑇 Se 𝑆 |
24 |
|
eqid |
⊢ OrdIso ( 𝑇 , 𝑆 ) = OrdIso ( 𝑇 , 𝑆 ) |
25 |
24
|
oieu |
⊢ ( ( 𝑇 We 𝑆 ∧ 𝑇 Se 𝑆 ) → ( ( Ord ( 𝐴 ↑o 𝐵 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) ) ↔ ( ( 𝐴 ↑o 𝐵 ) = dom OrdIso ( 𝑇 , 𝑆 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) = OrdIso ( 𝑇 , 𝑆 ) ) ) ) |
26 |
18 23 25
|
sylancl |
⊢ ( 𝜑 → ( ( Ord ( 𝐴 ↑o 𝐵 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) ) ↔ ( ( 𝐴 ↑o 𝐵 ) = dom OrdIso ( 𝑇 , 𝑆 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) = OrdIso ( 𝑇 , 𝑆 ) ) ) ) |
27 |
14 16 26
|
mpbi2and |
⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝐵 ) = dom OrdIso ( 𝑇 , 𝑆 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) = OrdIso ( 𝑇 , 𝑆 ) ) ) |
28 |
27
|
simprd |
⊢ ( 𝜑 → ◡ ( 𝐴 CNF 𝐵 ) = OrdIso ( 𝑇 , 𝑆 ) ) |
29 |
28
|
cnveqd |
⊢ ( 𝜑 → ◡ ◡ ( 𝐴 CNF 𝐵 ) = ◡ OrdIso ( 𝑇 , 𝑆 ) ) |
30 |
10 29
|
eqtr3d |
⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) = ◡ OrdIso ( 𝑇 , 𝑆 ) ) |