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

Metamath Proof Explorer

Theorem cantnfvalf

Description: Lemma for cantnf . The function appearing in cantnfval is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015)

Ref Expression
Hypothesis cantnfvalf.f ⊢ 𝐹 = seqω ( ( 𝑘 ∈ 𝐴 , 𝑧 ∈ 𝐵 ↦ ( 𝐶 +o 𝐷 ) ) , ∅ )
Assertion cantnfvalf 𝐹 : ω ⟶ On

Proof

Step Hyp Ref Expression
1 cantnfvalf.f ⊢ 𝐹 = seqω ( ( 𝑘 ∈ 𝐴 , 𝑧 ∈ 𝐵 ↦ ( 𝐶 +o 𝐷 ) ) , ∅ )
2 1 fnseqom ⊢ 𝐹 Fn ω
3 nn0suc ⊢ ( 𝑥 ∈ ω → ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ ω 𝑥 = suc 𝑦 ) )
4 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ∅ ) )
5 0ex ⊢ ∅ ∈ V
6 1 seqom0g ⊢ ( ∅ ∈ V → ( 𝐹 ‘ ∅ ) = ∅ )
7 5 6 ax-mp ⊢ ( 𝐹 ‘ ∅ ) = ∅
8 4 7 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝐹 ‘ 𝑥 ) = ∅ )
9 0elon ⊢ ∅ ∈ On
10 8 9 eqeltrdi ⊢ ( 𝑥 = ∅ → ( 𝐹 ‘ 𝑥 ) ∈ On )
11 1 seqomsuc ⊢ ( 𝑦 ∈ ω → ( 𝐹 ‘ suc 𝑦 ) = ( 𝑦 ( 𝑘 ∈ 𝐴 , 𝑧 ∈ 𝐵 ↦ ( 𝐶 +o 𝐷 ) ) ( 𝐹 ‘ 𝑦 ) ) )
12 df-ov ⊢ ( 𝑦 ( 𝑘 ∈ 𝐴 , 𝑧 ∈ 𝐵 ↦ ( 𝐶 +o 𝐷 ) ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝑘 ∈ 𝐴 , 𝑧 ∈ 𝐵 ↦ ( 𝐶 +o 𝐷 ) ) ‘ ⟨ 𝑦 , ( 𝐹 ‘ 𝑦 ) ⟩ )
13 11 12 eqtrdi ⊢ ( 𝑦 ∈ ω → ( 𝐹 ‘ suc 𝑦 ) = ( ( 𝑘 ∈ 𝐴 , 𝑧 ∈ 𝐵 ↦ ( 𝐶 +o 𝐷 ) ) ‘ ⟨ 𝑦 , ( 𝐹 ‘ 𝑦 ) ⟩ ) )
14 df-ov ⊢ ( 𝐶 +o 𝐷 ) = ( +o ‘ ⟨ 𝐶 , 𝐷 ⟩ )
15 fnoa ⊢ +o Fn ( On × On )
16 oacl ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 +o 𝑦 ) ∈ On )
17 16 rgen2 ⊢ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( 𝑥 +o 𝑦 ) ∈ On
18 ffnov ⊢ ( +o : ( On × On ) ⟶ On ↔ ( +o Fn ( On × On ) ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( 𝑥 +o 𝑦 ) ∈ On ) )
19 15 17 18 mpbir2an ⊢ +o : ( On × On ) ⟶ On
20 19 9 f0cli ⊢ ( +o ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ∈ On
21 14 20 eqeltri ⊢ ( 𝐶 +o 𝐷 ) ∈ On
22 21 rgen2w ⊢ ∀ 𝑘 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝐶 +o 𝐷 ) ∈ On
23 eqid ⊢ ( 𝑘 ∈ 𝐴 , 𝑧 ∈ 𝐵 ↦ ( 𝐶 +o 𝐷 ) ) = ( 𝑘 ∈ 𝐴 , 𝑧 ∈ 𝐵 ↦ ( 𝐶 +o 𝐷 ) )
24 23 fmpo ⊢ ( ∀ 𝑘 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝐶 +o 𝐷 ) ∈ On ↔ ( 𝑘 ∈ 𝐴 , 𝑧 ∈ 𝐵 ↦ ( 𝐶 +o 𝐷 ) ) : ( 𝐴 × 𝐵 ) ⟶ On )
25 22 24 mpbi ⊢ ( 𝑘 ∈ 𝐴 , 𝑧 ∈ 𝐵 ↦ ( 𝐶 +o 𝐷 ) ) : ( 𝐴 × 𝐵 ) ⟶ On
26 25 9 f0cli ⊢ ( ( 𝑘 ∈ 𝐴 , 𝑧 ∈ 𝐵 ↦ ( 𝐶 +o 𝐷 ) ) ‘ ⟨ 𝑦 , ( 𝐹 ‘ 𝑦 ) ⟩ ) ∈ On
27 13 26 eqeltrdi ⊢ ( 𝑦 ∈ ω → ( 𝐹 ‘ suc 𝑦 ) ∈ On )
28 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ suc 𝑦 ) )
29 28 eleq1d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∈ On ↔ ( 𝐹 ‘ suc 𝑦 ) ∈ On ) )
30 27 29 syl5ibrcom ⊢ ( 𝑦 ∈ ω → ( 𝑥 = suc 𝑦 → ( 𝐹 ‘ 𝑥 ) ∈ On ) )
31 30 rexlimiv ⊢ ( ∃ 𝑦 ∈ ω 𝑥 = suc 𝑦 → ( 𝐹 ‘ 𝑥 ) ∈ On )
32 10 31 jaoi ⊢ ( ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ ω 𝑥 = suc 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ On )
33 3 32 syl ⊢ ( 𝑥 ∈ ω → ( 𝐹 ‘ 𝑥 ) ∈ On )
34 33 rgen ⊢ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ On
35 ffnfv ⊢ ( 𝐹 : ω ⟶ On ↔ ( 𝐹 Fn ω ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ On ) )
36 2 34 35 mpbir2an ⊢ 𝐹 : ω ⟶ On