Step |
Hyp |
Ref |
Expression |
1 |
|
cantnfs.s |
⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 ) |
2 |
|
cantnfs.a |
⊢ ( 𝜑 → 𝐴 ∈ On ) |
3 |
|
cantnfs.b |
⊢ ( 𝜑 → 𝐵 ∈ On ) |
4 |
|
oemapval.t |
⊢ 𝑇 = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } |
5 |
|
cantnf.c |
⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ↑o 𝐵 ) ) |
6 |
|
cantnf.s |
⊢ ( 𝜑 → 𝐶 ⊆ ran ( 𝐴 CNF 𝐵 ) ) |
7 |
|
cantnf.e |
⊢ ( 𝜑 → ∅ ∈ 𝐶 ) |
8 |
|
oecl |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On ) |
9 |
2 3 8
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 ↑o 𝐵 ) ∈ On ) |
10 |
|
onelon |
⊢ ( ( ( 𝐴 ↑o 𝐵 ) ∈ On ∧ 𝐶 ∈ ( 𝐴 ↑o 𝐵 ) ) → 𝐶 ∈ On ) |
11 |
9 5 10
|
syl2anc |
⊢ ( 𝜑 → 𝐶 ∈ On ) |
12 |
|
ondif1 |
⊢ ( 𝐶 ∈ ( On ∖ 1o ) ↔ ( 𝐶 ∈ On ∧ ∅ ∈ 𝐶 ) ) |
13 |
11 7 12
|
sylanbrc |
⊢ ( 𝜑 → 𝐶 ∈ ( On ∖ 1o ) ) |
14 |
13
|
eldifbd |
⊢ ( 𝜑 → ¬ 𝐶 ∈ 1o ) |
15 |
|
ssel |
⊢ ( ( 𝐴 ↑o 𝐵 ) ⊆ 1o → ( 𝐶 ∈ ( 𝐴 ↑o 𝐵 ) → 𝐶 ∈ 1o ) ) |
16 |
5 15
|
syl5com |
⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝐵 ) ⊆ 1o → 𝐶 ∈ 1o ) ) |
17 |
14 16
|
mtod |
⊢ ( 𝜑 → ¬ ( 𝐴 ↑o 𝐵 ) ⊆ 1o ) |
18 |
|
oe0m |
⊢ ( 𝐵 ∈ On → ( ∅ ↑o 𝐵 ) = ( 1o ∖ 𝐵 ) ) |
19 |
3 18
|
syl |
⊢ ( 𝜑 → ( ∅ ↑o 𝐵 ) = ( 1o ∖ 𝐵 ) ) |
20 |
|
difss |
⊢ ( 1o ∖ 𝐵 ) ⊆ 1o |
21 |
19 20
|
eqsstrdi |
⊢ ( 𝜑 → ( ∅ ↑o 𝐵 ) ⊆ 1o ) |
22 |
|
oveq1 |
⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o 𝐵 ) = ( ∅ ↑o 𝐵 ) ) |
23 |
22
|
sseq1d |
⊢ ( 𝐴 = ∅ → ( ( 𝐴 ↑o 𝐵 ) ⊆ 1o ↔ ( ∅ ↑o 𝐵 ) ⊆ 1o ) ) |
24 |
21 23
|
syl5ibrcom |
⊢ ( 𝜑 → ( 𝐴 = ∅ → ( 𝐴 ↑o 𝐵 ) ⊆ 1o ) ) |
25 |
|
oe1m |
⊢ ( 𝐵 ∈ On → ( 1o ↑o 𝐵 ) = 1o ) |
26 |
|
eqimss |
⊢ ( ( 1o ↑o 𝐵 ) = 1o → ( 1o ↑o 𝐵 ) ⊆ 1o ) |
27 |
3 25 26
|
3syl |
⊢ ( 𝜑 → ( 1o ↑o 𝐵 ) ⊆ 1o ) |
28 |
|
oveq1 |
⊢ ( 𝐴 = 1o → ( 𝐴 ↑o 𝐵 ) = ( 1o ↑o 𝐵 ) ) |
29 |
28
|
sseq1d |
⊢ ( 𝐴 = 1o → ( ( 𝐴 ↑o 𝐵 ) ⊆ 1o ↔ ( 1o ↑o 𝐵 ) ⊆ 1o ) ) |
30 |
27 29
|
syl5ibrcom |
⊢ ( 𝜑 → ( 𝐴 = 1o → ( 𝐴 ↑o 𝐵 ) ⊆ 1o ) ) |
31 |
24 30
|
jaod |
⊢ ( 𝜑 → ( ( 𝐴 = ∅ ∨ 𝐴 = 1o ) → ( 𝐴 ↑o 𝐵 ) ⊆ 1o ) ) |
32 |
17 31
|
mtod |
⊢ ( 𝜑 → ¬ ( 𝐴 = ∅ ∨ 𝐴 = 1o ) ) |
33 |
|
elpri |
⊢ ( 𝐴 ∈ { ∅ , 1o } → ( 𝐴 = ∅ ∨ 𝐴 = 1o ) ) |
34 |
|
df2o3 |
⊢ 2o = { ∅ , 1o } |
35 |
33 34
|
eleq2s |
⊢ ( 𝐴 ∈ 2o → ( 𝐴 = ∅ ∨ 𝐴 = 1o ) ) |
36 |
32 35
|
nsyl |
⊢ ( 𝜑 → ¬ 𝐴 ∈ 2o ) |
37 |
2 36
|
eldifd |
⊢ ( 𝜑 → 𝐴 ∈ ( On ∖ 2o ) ) |
38 |
37 13
|
jca |
⊢ ( 𝜑 → ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐶 ∈ ( On ∖ 1o ) ) ) |