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