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

Metamath Proof Explorer

Theorem dcomex

Description: The Axiom of Dependent Choice implies Infinity, the way we have stated it. Thus, we haveInf+AC impliesDC andDC impliesInf, but AC does not implyInf. (Contributed by Mario Carneiro, 25-Jan-2013)

Ref Expression
Assertion dcomex ω ∈ V

Proof

Step Hyp Ref Expression
1 1n0 ⊢ 1o ≠ ∅
2 df-br ⊢ ( ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 ) ↔ ⟨ ( 𝑓 ‘ 𝑛 ) , ( 𝑓 ‘ suc 𝑛 ) ⟩ ∈ { ⟨ 1o , 1o ⟩ } )
3 elsni ⊢ ( ⟨ ( 𝑓 ‘ 𝑛 ) , ( 𝑓 ‘ suc 𝑛 ) ⟩ ∈ { ⟨ 1o , 1o ⟩ } → ⟨ ( 𝑓 ‘ 𝑛 ) , ( 𝑓 ‘ suc 𝑛 ) ⟩ = ⟨ 1o , 1o ⟩ )
4 fvex ⊢ ( 𝑓 ‘ 𝑛 ) ∈ V
5 fvex ⊢ ( 𝑓 ‘ suc 𝑛 ) ∈ V
6 4 5 opth1 ⊢ ( ⟨ ( 𝑓 ‘ 𝑛 ) , ( 𝑓 ‘ suc 𝑛 ) ⟩ = ⟨ 1o , 1o ⟩ → ( 𝑓 ‘ 𝑛 ) = 1o )
7 3 6 syl ⊢ ( ⟨ ( 𝑓 ‘ 𝑛 ) , ( 𝑓 ‘ suc 𝑛 ) ⟩ ∈ { ⟨ 1o , 1o ⟩ } → ( 𝑓 ‘ 𝑛 ) = 1o )
8 2 7 sylbi ⊢ ( ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 ) → ( 𝑓 ‘ 𝑛 ) = 1o )
9 tz6.12i ⊢ ( 1o ≠ ∅ → ( ( 𝑓 ‘ 𝑛 ) = 1o → 𝑛 𝑓 1o ) )
10 1 8 9 mpsyl ⊢ ( ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 ) → 𝑛 𝑓 1o )
11 vex ⊢ 𝑛 ∈ V
12 1oex ⊢ 1o ∈ V
13 11 12 breldm ⊢ ( 𝑛 𝑓 1o → 𝑛 ∈ dom 𝑓 )
14 10 13 syl ⊢ ( ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 ) → 𝑛 ∈ dom 𝑓 )
15 14 ralimi ⊢ ( ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 ) → ∀ 𝑛 ∈ ω 𝑛 ∈ dom 𝑓 )
16 dfss3 ⊢ ( ω ⊆ dom 𝑓 ↔ ∀ 𝑛 ∈ ω 𝑛 ∈ dom 𝑓 )
17 15 16 sylibr ⊢ ( ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 ) → ω ⊆ dom 𝑓 )
18 vex ⊢ 𝑓 ∈ V
19 18 dmex ⊢ dom 𝑓 ∈ V
20 19 ssex ⊢ ( ω ⊆ dom 𝑓 → ω ∈ V )
21 17 20 syl ⊢ ( ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 ) → ω ∈ V )
22 snex ⊢ { ⟨ 1o , 1o ⟩ } ∈ V
23 12 12 fvsn ⊢ ( { ⟨ 1o , 1o ⟩ } ‘ 1o ) = 1o
24 12 12 funsn ⊢ Fun { ⟨ 1o , 1o ⟩ }
25 12 snid ⊢ 1o ∈ { 1o }
26 12 dmsnop ⊢ dom { ⟨ 1o , 1o ⟩ } = { 1o }
27 25 26 eleqtrri ⊢ 1o ∈ dom { ⟨ 1o , 1o ⟩ }
28 funbrfvb ⊢ ( ( Fun { ⟨ 1o , 1o ⟩ } ∧ 1o ∈ dom { ⟨ 1o , 1o ⟩ } ) → ( ( { ⟨ 1o , 1o ⟩ } ‘ 1o ) = 1o ↔ 1o { ⟨ 1o , 1o ⟩ } 1o ) )
29 24 27 28 mp2an ⊢ ( ( { ⟨ 1o , 1o ⟩ } ‘ 1o ) = 1o ↔ 1o { ⟨ 1o , 1o ⟩ } 1o )
30 23 29 mpbi ⊢ 1o { ⟨ 1o , 1o ⟩ } 1o
31 breq12 ⊢ ( ( 𝑠 = 1o ∧ 𝑡 = 1o ) → ( 𝑠 { ⟨ 1o , 1o ⟩ } 𝑡 ↔ 1o { ⟨ 1o , 1o ⟩ } 1o ) )
32 12 12 31 spc2ev ⊢ ( 1o { ⟨ 1o , 1o ⟩ } 1o → ∃ 𝑠 ∃ 𝑡 𝑠 { ⟨ 1o , 1o ⟩ } 𝑡 )
33 30 32 ax-mp ⊢ ∃ 𝑠 ∃ 𝑡 𝑠 { ⟨ 1o , 1o ⟩ } 𝑡
34 breq ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → ( 𝑠 𝑥 𝑡 ↔ 𝑠 { ⟨ 1o , 1o ⟩ } 𝑡 ) )
35 34 2exbidv ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → ( ∃ 𝑠 ∃ 𝑡 𝑠 𝑥 𝑡 ↔ ∃ 𝑠 ∃ 𝑡 𝑠 { ⟨ 1o , 1o ⟩ } 𝑡 ) )
36 33 35 mpbiri ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → ∃ 𝑠 ∃ 𝑡 𝑠 𝑥 𝑡 )
37 ssid ⊢ { 1o } ⊆ { 1o }
38 12 rnsnop ⊢ ran { ⟨ 1o , 1o ⟩ } = { 1o }
39 37 38 26 3sstr4i ⊢ ran { ⟨ 1o , 1o ⟩ } ⊆ dom { ⟨ 1o , 1o ⟩ }
40 rneq ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → ran 𝑥 = ran { ⟨ 1o , 1o ⟩ } )
41 dmeq ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → dom 𝑥 = dom { ⟨ 1o , 1o ⟩ } )
42 40 41 sseq12d ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → ( ran 𝑥 ⊆ dom 𝑥 ↔ ran { ⟨ 1o , 1o ⟩ } ⊆ dom { ⟨ 1o , 1o ⟩ } ) )
43 39 42 mpbiri ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → ran 𝑥 ⊆ dom 𝑥 )
44 pm5.5 ⊢ ( ( ∃ 𝑠 ∃ 𝑡 𝑠 𝑥 𝑡 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ( ( ( ∃ 𝑠 ∃ 𝑡 𝑠 𝑥 𝑡 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) ↔ ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) )
45 36 43 44 syl2anc ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → ( ( ( ∃ 𝑠 ∃ 𝑡 𝑠 𝑥 𝑡 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) ↔ ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) )
46 breq ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → ( ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ↔ ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 ) ) )
47 46 ralbidv ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → ( ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ↔ ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 ) ) )
48 47 exbidv ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → ( ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ↔ ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 ) ) )
49 45 48 bitrd ⊢ ( 𝑥 = { ⟨ 1o , 1o ⟩ } → ( ( ( ∃ 𝑠 ∃ 𝑡 𝑠 𝑥 𝑡 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) ↔ ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 ) ) )
50 ax-dc ⊢ ( ( ∃ 𝑠 ∃ 𝑡 𝑠 𝑥 𝑡 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) )
51 22 49 50 vtocl ⊢ ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) { ⟨ 1o , 1o ⟩ } ( 𝑓 ‘ suc 𝑛 )
52 21 51 exlimiiv ⊢ ω ∈ V