Metamath Proof Explorer

Theorem cantnflem4

Description: Lemma for cantnf . Complete the induction step of cantnflem3 . (Contributed by Mario Carneiro, 25-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 ⊢ ( 𝜑 → ∅ ∈ 𝐶 )
cantnf.x ⊢ 𝑋 = ∪ ∩ { 𝑐 ∈ On ∣ 𝐶 ∈ ( 𝐴 ↑o 𝑐 ) }
cantnf.p ⊢ 𝑃 = ( ℩ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴 ↑o 𝑋 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑎 ) +o 𝑏 ) = 𝐶 ) )
cantnf.y ⊢ 𝑌 = ( 1st ‘ 𝑃 )
cantnf.z ⊢ 𝑍 = ( 2nd ‘ 𝑃 )
Assertion cantnflem4 ( 𝜑 → 𝐶 ∈ ran ( 𝐴 CNF 𝐵 ) )

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 cantnf.x ⊢ 𝑋 = ∪ ∩ { 𝑐 ∈ On ∣ 𝐶 ∈ ( 𝐴 ↑o 𝑐 ) }
9 cantnf.p ⊢ 𝑃 = ( ℩ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴 ↑o 𝑋 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑎 ) +o 𝑏 ) = 𝐶 ) )
10 cantnf.y ⊢ 𝑌 = ( 1st ‘ 𝑃 )
11 cantnf.z ⊢ 𝑍 = ( 2nd ‘ 𝑃 )
12 1 2 3 4 5 6 7 cantnflem2 ⊢ ( 𝜑 → ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐶 ∈ ( On ∖ 1o ) ) )
13 eqid ⊢ 𝑋 = 𝑋
14 eqid ⊢ 𝑌 = 𝑌
15 eqid ⊢ 𝑍 = 𝑍
16 13 14 15 3pm3.2i ⊢ ( 𝑋 = 𝑋 ∧ 𝑌 = 𝑌 ∧ 𝑍 = 𝑍 )
17 8 9 10 11 oeeui ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐶 ∈ ( On ∖ 1o ) ) → ( ( ( 𝑋 ∈ On ∧ 𝑌 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) ∧ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) = 𝐶 ) ↔ ( 𝑋 = 𝑋 ∧ 𝑌 = 𝑌 ∧ 𝑍 = 𝑍 ) ) )
18 16 17 mpbiri ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐶 ∈ ( On ∖ 1o ) ) → ( ( 𝑋 ∈ On ∧ 𝑌 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) ∧ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) = 𝐶 ) )
19 12 18 syl ⊢ ( 𝜑 → ( ( 𝑋 ∈ On ∧ 𝑌 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) ∧ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) = 𝐶 ) )
20 19 simpld ⊢ ( 𝜑 → ( 𝑋 ∈ On ∧ 𝑌 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) )
21 20 simp1d ⊢ ( 𝜑 → 𝑋 ∈ On )
22 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ On ) → ( 𝐴 ↑o 𝑋 ) ∈ On )
23 2 21 22 syl2anc ⊢ ( 𝜑 → ( 𝐴 ↑o 𝑋 ) ∈ On )
24 20 simp2d ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 ∖ 1o ) )
25 24 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
26 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ On )
27 2 25 26 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ On )
28 omcl ⊢ ( ( ( 𝐴 ↑o 𝑋 ) ∈ On ∧ 𝑌 ∈ On ) → ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) ∈ On )
29 23 27 28 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) ∈ On )
30 20 simp3d ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) )
31 onelon ⊢ ( ( ( 𝐴 ↑o 𝑋 ) ∈ On ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) → 𝑍 ∈ On )
32 23 30 31 syl2anc ⊢ ( 𝜑 → 𝑍 ∈ On )
33 oaword1 ⊢ ( ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) ∈ On ∧ 𝑍 ∈ On ) → ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) ⊆ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) )
34 29 32 33 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) ⊆ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) )
35 dif1o ⊢ ( 𝑌 ∈ ( 𝐴 ∖ 1o ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≠ ∅ ) )
36 35 simprbi ⊢ ( 𝑌 ∈ ( 𝐴 ∖ 1o ) → 𝑌 ≠ ∅ )
37 24 36 syl ⊢ ( 𝜑 → 𝑌 ≠ ∅ )
38 on0eln0 ⊢ ( 𝑌 ∈ On → ( ∅ ∈ 𝑌 ↔ 𝑌 ≠ ∅ ) )
39 27 38 syl ⊢ ( 𝜑 → ( ∅ ∈ 𝑌 ↔ 𝑌 ≠ ∅ ) )
40 37 39 mpbird ⊢ ( 𝜑 → ∅ ∈ 𝑌 )
41 omword1 ⊢ ( ( ( ( 𝐴 ↑o 𝑋 ) ∈ On ∧ 𝑌 ∈ On ) ∧ ∅ ∈ 𝑌 ) → ( 𝐴 ↑o 𝑋 ) ⊆ ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) )
42 23 27 40 41 syl21anc ⊢ ( 𝜑 → ( 𝐴 ↑o 𝑋 ) ⊆ ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) )
43 42 30 sseldd ⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) )
44 34 43 sseldd ⊢ ( 𝜑 → 𝑍 ∈ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) )
45 19 simprd ⊢ ( 𝜑 → ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) = 𝐶 )
46 44 45 eleqtrd ⊢ ( 𝜑 → 𝑍 ∈ 𝐶 )
47 6 46 sseldd ⊢ ( 𝜑 → 𝑍 ∈ ran ( 𝐴 CNF 𝐵 ) )
48 1 2 3 cantnff ⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴 ↑o 𝐵 ) )
49 ffn ⊢ ( ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴 ↑o 𝐵 ) → ( 𝐴 CNF 𝐵 ) Fn 𝑆 )
50 fvelrnb ⊢ ( ( 𝐴 CNF 𝐵 ) Fn 𝑆 → ( 𝑍 ∈ ran ( 𝐴 CNF 𝐵 ) ↔ ∃ 𝑔 ∈ 𝑆 ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 ) )
51 48 49 50 3syl ⊢ ( 𝜑 → ( 𝑍 ∈ ran ( 𝐴 CNF 𝐵 ) ↔ ∃ 𝑔 ∈ 𝑆 ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 ) )
52 47 51 mpbid ⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝑆 ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 )
53 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 ) ) → 𝐴 ∈ On )
54 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 ) ) → 𝐵 ∈ On )
55 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 ) ) → 𝐶 ∈ ( 𝐴 ↑o 𝐵 ) )
56 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 ) ) → 𝐶 ⊆ ran ( 𝐴 CNF 𝐵 ) )
57 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 ) ) → ∅ ∈ 𝐶 )
58 simprl ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 ) ) → 𝑔 ∈ 𝑆 )
59 simprr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 )
60 eqid ⊢ ( 𝑡 ∈ 𝐵 ↦ if ( 𝑡 = 𝑋 , 𝑌 , ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝐵 ↦ if ( 𝑡 = 𝑋 , 𝑌 , ( 𝑔 ‘ 𝑡 ) ) )
61 1 53 54 4 55 56 57 8 9 10 11 58 59 60 cantnflem3 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) = 𝑍 ) ) → 𝐶 ∈ ran ( 𝐴 CNF 𝐵 ) )
62 52 61 rexlimddv ⊢ ( 𝜑 → 𝐶 ∈ ran ( 𝐴 CNF 𝐵 ) )