Step |
Hyp |
Ref |
Expression |
1 |
|
cantnff1o.1 |
⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 ) |
2 |
|
cantnff1o.2 |
⊢ ( 𝜑 → 𝐴 ∈ On ) |
3 |
|
cantnff1o.3 |
⊢ ( 𝜑 → 𝐵 ∈ On ) |
4 |
|
eqid |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } |
5 |
1 2 3 4
|
cantnf |
⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) Isom { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) ) |
6 |
|
isof1o |
⊢ ( ( 𝐴 CNF 𝐵 ) Isom { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) → ( 𝐴 CNF 𝐵 ) : 𝑆 –1-1-onto→ ( 𝐴 ↑o 𝐵 ) ) |
7 |
5 6
|
syl |
⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆 –1-1-onto→ ( 𝐴 ↑o 𝐵 ) ) |