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

Metamath Proof Explorer

Theorem axdclem2

Description: Lemma for axdc . Using the full Axiom of Choice, we can construct a choice function g on ~P dom x . From this, we can build a sequence F starting at any value s e. dom x by repeatedly applying g to the set ( Fx ) (where x is the value from the previous iteration). (Contributed by Mario Carneiro, 25-Jan-2013)

Ref Expression
Hypothesis axdclem2.1 ⊢ 𝐹 = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) ) , 𝑠 ) ↾ ω )
Assertion axdclem2 ( ∃ 𝑧 𝑠 𝑥 𝑧 → ( ran 𝑥 ⊆ dom 𝑥 → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 axdclem2.1 ⊢ 𝐹 = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) ) , 𝑠 ) ↾ ω )
2 frfnom ⊢ ( rec ( ( 𝑦 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) ) , 𝑠 ) ↾ ω ) Fn ω
3 1 fneq1i ⊢ ( 𝐹 Fn ω ↔ ( rec ( ( 𝑦 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) ) , 𝑠 ) ↾ ω ) Fn ω )
4 2 3 mpbir ⊢ 𝐹 Fn ω
5 4 a1i ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ∃ 𝑧 𝑠 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → 𝐹 Fn ω )
6 omex ⊢ ω ∈ V
7 6 a1i ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ∃ 𝑧 𝑠 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ω ∈ V )
8 5 7 fnexd ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ∃ 𝑧 𝑠 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → 𝐹 ∈ V )
9 fveq2 ⊢ ( 𝑛 = ∅ → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ∅ ) )
10 suceq ⊢ ( 𝑛 = ∅ → suc 𝑛 = suc ∅ )
11 10 fveq2d ⊢ ( 𝑛 = ∅ → ( 𝐹 ‘ suc 𝑛 ) = ( 𝐹 ‘ suc ∅ ) )
12 9 11 breq12d ⊢ ( 𝑛 = ∅ → ( ( 𝐹 ‘ 𝑛 ) 𝑥 ( 𝐹 ‘ suc 𝑛 ) ↔ ( 𝐹 ‘ ∅ ) 𝑥 ( 𝐹 ‘ suc ∅ ) ) )
13 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
14 suceq ⊢ ( 𝑛 = 𝑘 → suc 𝑛 = suc 𝑘 )
15 14 fveq2d ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ suc 𝑛 ) = ( 𝐹 ‘ suc 𝑘 ) )
16 13 15 breq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) 𝑥 ( 𝐹 ‘ suc 𝑛 ) ↔ ( 𝐹 ‘ 𝑘 ) 𝑥 ( 𝐹 ‘ suc 𝑘 ) ) )
17 fveq2 ⊢ ( 𝑛 = suc 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ suc 𝑘 ) )
18 suceq ⊢ ( 𝑛 = suc 𝑘 → suc 𝑛 = suc suc 𝑘 )
19 18 fveq2d ⊢ ( 𝑛 = suc 𝑘 → ( 𝐹 ‘ suc 𝑛 ) = ( 𝐹 ‘ suc suc 𝑘 ) )
20 17 19 breq12d ⊢ ( 𝑛 = suc 𝑘 → ( ( 𝐹 ‘ 𝑛 ) 𝑥 ( 𝐹 ‘ suc 𝑛 ) ↔ ( 𝐹 ‘ suc 𝑘 ) 𝑥 ( 𝐹 ‘ suc suc 𝑘 ) ) )
21 1 fveq1i ⊢ ( 𝐹 ‘ ∅ ) = ( ( rec ( ( 𝑦 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) ) , 𝑠 ) ↾ ω ) ‘ ∅ )
22 fr0g ⊢ ( 𝑠 ∈ V → ( ( rec ( ( 𝑦 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) ) , 𝑠 ) ↾ ω ) ‘ ∅ ) = 𝑠 )
23 22 elv ⊢ ( ( rec ( ( 𝑦 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) ) , 𝑠 ) ↾ ω ) ‘ ∅ ) = 𝑠
24 21 23 eqtri ⊢ ( 𝐹 ‘ ∅ ) = 𝑠
25 24 breq1i ⊢ ( ( 𝐹 ‘ ∅ ) 𝑥 𝑧 ↔ 𝑠 𝑥 𝑧 )
26 25 biimpri ⊢ ( 𝑠 𝑥 𝑧 → ( 𝐹 ‘ ∅ ) 𝑥 𝑧 )
27 26 eximi ⊢ ( ∃ 𝑧 𝑠 𝑥 𝑧 → ∃ 𝑧 ( 𝐹 ‘ ∅ ) 𝑥 𝑧 )
28 peano1 ⊢ ∅ ∈ ω
29 1 axdclem ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃ 𝑧 ( 𝐹 ‘ ∅ ) 𝑥 𝑧 ) → ( ∅ ∈ ω → ( 𝐹 ‘ ∅ ) 𝑥 ( 𝐹 ‘ suc ∅ ) ) )
30 28 29 mpi ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃ 𝑧 ( 𝐹 ‘ ∅ ) 𝑥 𝑧 ) → ( 𝐹 ‘ ∅ ) 𝑥 ( 𝐹 ‘ suc ∅ ) )
31 27 30 syl3an3 ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃ 𝑧 𝑠 𝑥 𝑧 ) → ( 𝐹 ‘ ∅ ) 𝑥 ( 𝐹 ‘ suc ∅ ) )
32 31 3com23 ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ∃ 𝑧 𝑠 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ( 𝐹 ‘ ∅ ) 𝑥 ( 𝐹 ‘ suc ∅ ) )
33 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
34 fvex ⊢ ( 𝐹 ‘ suc 𝑘 ) ∈ V
35 33 34 brelrn ⊢ ( ( 𝐹 ‘ 𝑘 ) 𝑥 ( 𝐹 ‘ suc 𝑘 ) → ( 𝐹 ‘ suc 𝑘 ) ∈ ran 𝑥 )
36 ssel ⊢ ( ran 𝑥 ⊆ dom 𝑥 → ( ( 𝐹 ‘ suc 𝑘 ) ∈ ran 𝑥 → ( 𝐹 ‘ suc 𝑘 ) ∈ dom 𝑥 ) )
37 35 36 syl5 ⊢ ( ran 𝑥 ⊆ dom 𝑥 → ( ( 𝐹 ‘ 𝑘 ) 𝑥 ( 𝐹 ‘ suc 𝑘 ) → ( 𝐹 ‘ suc 𝑘 ) ∈ dom 𝑥 ) )
38 34 eldm ⊢ ( ( 𝐹 ‘ suc 𝑘 ) ∈ dom 𝑥 ↔ ∃ 𝑧 ( 𝐹 ‘ suc 𝑘 ) 𝑥 𝑧 )
39 37 38 imbitrdi ⊢ ( ran 𝑥 ⊆ dom 𝑥 → ( ( 𝐹 ‘ 𝑘 ) 𝑥 ( 𝐹 ‘ suc 𝑘 ) → ∃ 𝑧 ( 𝐹 ‘ suc 𝑘 ) 𝑥 𝑧 ) )
40 39 ad2antll ⊢ ( ( 𝑘 ∈ ω ∧ ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝑥 ( 𝐹 ‘ suc 𝑘 ) → ∃ 𝑧 ( 𝐹 ‘ suc 𝑘 ) 𝑥 𝑧 ) )
41 peano2 ⊢ ( 𝑘 ∈ ω → suc 𝑘 ∈ ω )
42 1 axdclem ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃ 𝑧 ( 𝐹 ‘ suc 𝑘 ) 𝑥 𝑧 ) → ( suc 𝑘 ∈ ω → ( 𝐹 ‘ suc 𝑘 ) 𝑥 ( 𝐹 ‘ suc suc 𝑘 ) ) )
43 41 42 syl5 ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃ 𝑧 ( 𝐹 ‘ suc 𝑘 ) 𝑥 𝑧 ) → ( 𝑘 ∈ ω → ( 𝐹 ‘ suc 𝑘 ) 𝑥 ( 𝐹 ‘ suc suc 𝑘 ) ) )
44 43 3expia ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ) → ( ∃ 𝑧 ( 𝐹 ‘ suc 𝑘 ) 𝑥 𝑧 → ( 𝑘 ∈ ω → ( 𝐹 ‘ suc 𝑘 ) 𝑥 ( 𝐹 ‘ suc suc 𝑘 ) ) ) )
45 44 com3r ⊢ ( 𝑘 ∈ ω → ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ) → ( ∃ 𝑧 ( 𝐹 ‘ suc 𝑘 ) 𝑥 𝑧 → ( 𝐹 ‘ suc 𝑘 ) 𝑥 ( 𝐹 ‘ suc suc 𝑘 ) ) ) )
46 45 imp ⊢ ( ( 𝑘 ∈ ω ∧ ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ) ) → ( ∃ 𝑧 ( 𝐹 ‘ suc 𝑘 ) 𝑥 𝑧 → ( 𝐹 ‘ suc 𝑘 ) 𝑥 ( 𝐹 ‘ suc suc 𝑘 ) ) )
47 40 46 syld ⊢ ( ( 𝑘 ∈ ω ∧ ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝑥 ( 𝐹 ‘ suc 𝑘 ) → ( 𝐹 ‘ suc 𝑘 ) 𝑥 ( 𝐹 ‘ suc suc 𝑘 ) ) )
48 47 3adantr2 ⊢ ( ( 𝑘 ∈ ω ∧ ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ∃ 𝑧 𝑠 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝑥 ( 𝐹 ‘ suc 𝑘 ) → ( 𝐹 ‘ suc 𝑘 ) 𝑥 ( 𝐹 ‘ suc suc 𝑘 ) ) )
49 48 ex ⊢ ( 𝑘 ∈ ω → ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ∃ 𝑧 𝑠 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ( ( 𝐹 ‘ 𝑘 ) 𝑥 ( 𝐹 ‘ suc 𝑘 ) → ( 𝐹 ‘ suc 𝑘 ) 𝑥 ( 𝐹 ‘ suc suc 𝑘 ) ) ) )
50 12 16 20 32 49 finds2 ⊢ ( 𝑛 ∈ ω → ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ∃ 𝑧 𝑠 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ( 𝐹 ‘ 𝑛 ) 𝑥 ( 𝐹 ‘ suc 𝑛 ) ) )
51 50 com12 ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ∃ 𝑧 𝑠 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ( 𝑛 ∈ ω → ( 𝐹 ‘ 𝑛 ) 𝑥 ( 𝐹 ‘ suc 𝑛 ) ) )
52 51 ralrimiv ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ∃ 𝑧 𝑠 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ∀ 𝑛 ∈ ω ( 𝐹 ‘ 𝑛 ) 𝑥 ( 𝐹 ‘ suc 𝑛 ) )
53 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
54 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ suc 𝑛 ) = ( 𝐹 ‘ suc 𝑛 ) )
55 53 54 breq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ↔ ( 𝐹 ‘ 𝑛 ) 𝑥 ( 𝐹 ‘ suc 𝑛 ) ) )
56 55 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ↔ ∀ 𝑛 ∈ ω ( 𝐹 ‘ 𝑛 ) 𝑥 ( 𝐹 ‘ suc 𝑛 ) ) )
57 8 52 56 spcedv ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ∃ 𝑧 𝑠 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) )
58 57 3exp ⊢ ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( ∃ 𝑧 𝑠 𝑥 𝑧 → ( ran 𝑥 ⊆ dom 𝑥 → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) ) )
59 vex ⊢ 𝑥 ∈ V
60 59 dmex ⊢ dom 𝑥 ∈ V
61 60 pwex ⊢ 𝒫 dom 𝑥 ∈ V
62 61 ac4c ⊢ ∃ 𝑔 ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 )
63 58 62 exlimiiv ⊢ ( ∃ 𝑧 𝑠 𝑥 𝑧 → ( ran 𝑥 ⊆ dom 𝑥 → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) )