This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cantnflem2

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
cantnf.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ↑o 𝐵 ) )
cantnf.s ⊢ ( 𝜑 → 𝐶 ⊆ ran ( 𝐴 CNF 𝐵 ) )
cantnf.e ⊢ ( 𝜑 → ∅ ∈ 𝐶 )
Assertion cantnflem2 ( 𝜑 → ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐶 ∈ ( On ∖ 1o ) ) )

Proof

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 ) ) )