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