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