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 → ( 1oo 𝐵 ) = 1o )
26 eqimss ( ( 1oo 𝐵 ) = 1o → ( 1oo 𝐵 ) ⊆ 1o )
27 3 25 26 3syl ( 𝜑 → ( 1oo 𝐵 ) ⊆ 1o )
28 oveq1 ( 𝐴 = 1o → ( 𝐴o 𝐵 ) = ( 1oo 𝐵 ) )
29 28 sseq1d ( 𝐴 = 1o → ( ( 𝐴o 𝐵 ) ⊆ 1o ↔ ( 1oo 𝐵 ) ⊆ 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 ) ) )