Theorem dfacacn 9248

Description: A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015.)

Assertion

Ref	Expression
dfacacn	⊢ (CHOICE ↔ ∀𝑥AC 𝑥 = V)

Proof of Theorem dfacacn

Dummy variables 𝑓 𝑔 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		acacni 9247	. . . 4 ⊢ ((CHOICE ∧ 𝑥 ∈ V) → AC 𝑥 = V)
2	1	elvd 3396	. . 3 ⊢ (CHOICE → AC 𝑥 = V)
3	2	alrimiv 2018	. 2 ⊢ (CHOICE → ∀𝑥AC 𝑥 = V)
4		vex 3394	. . . . . . 7 ⊢ 𝑦 ∈ V
5		difexg 5003	. . . . . . 7 ⊢ (𝑦 ∈ V → (𝑦 ∖ {∅}) ∈ V)
6	4, 5	ax-mp 5	. . . . . 6 ⊢ (𝑦 ∖ {∅}) ∈ V
7		acneq 9149	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∖ {∅}) → AC 𝑥 = AC (𝑦 ∖ {∅}))
8	7	eqeq1d 2808	. . . . . 6 ⊢ (𝑥 = (𝑦 ∖ {∅}) → (AC 𝑥 = V ↔ AC (𝑦 ∖ {∅}) = V))
9	6, 8	spcv 3492	. . . . 5 ⊢ (∀𝑥AC 𝑥 = V → AC (𝑦 ∖ {∅}) = V)
10		vuniex 7184	. . . . . . 7 ⊢ ∪ 𝑦 ∈ V
11		id 22	. . . . . . 7 ⊢ (AC (𝑦 ∖ {∅}) = V → AC (𝑦 ∖ {∅}) = V)
12	10, 11	syl5eleqr 2892	. . . . . 6 ⊢ (AC (𝑦 ∖ {∅}) = V → ∪ 𝑦 ∈ AC (𝑦 ∖ {∅}))
13		eldifi 3931	. . . . . . . . 9 ⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → 𝑧 ∈ 𝑦)
14		elssuni 4661	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝑦 → 𝑧 ⊆ ∪ 𝑦)
15	13, 14	syl 17	. . . . . . . 8 ⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → 𝑧 ⊆ ∪ 𝑦)
16		eldifsni 4512	. . . . . . . 8 ⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → 𝑧 ≠ ∅)
17	15, 16	jca 503	. . . . . . 7 ⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → (𝑧 ⊆ ∪ 𝑦 ∧ 𝑧 ≠ ∅))
18	17	rgen 3110	. . . . . 6 ⊢ ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑧 ⊆ ∪ 𝑦 ∧ 𝑧 ≠ ∅)
19		acni2 9152	. . . . . 6 ⊢ ((∪ 𝑦 ∈ AC (𝑦 ∖ {∅}) ∧ ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑧 ⊆ ∪ 𝑦 ∧ 𝑧 ≠ ∅)) → ∃𝑔(𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦 ∧ ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧))
20	12, 18, 19	sylancl 576	. . . . 5 ⊢ (AC (𝑦 ∖ {∅}) = V → ∃𝑔(𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦 ∧ ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧))
21	4	mptex 6711	. . . . . . 7 ⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) ∈ V
22		simpr 473	. . . . . . . . 9 ⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦 ∧ ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧)
23		eldifsn 4508	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑦 ∖ {∅}) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅))
24	23	imbi1i 340	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ (𝑦 ∖ {∅}) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))
25		fveq2 6408	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝑔‘𝑥) = (𝑔‘𝑧))
26		eqid 2806	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))
27		fvex 6421	. . . . . . . . . . . . . . 15 ⊢ (𝑔‘𝑧) ∈ V
28	25, 26, 27	fvmpt 6503	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝑦 → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) = (𝑔‘𝑧))
29	13, 28	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) = (𝑔‘𝑧))
30	29	eleq1d 2870	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → (((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧 ↔ (𝑔‘𝑧) ∈ 𝑧))
31	30	pm5.74i 262	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ (𝑦 ∖ {∅}) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧) ↔ (𝑧 ∈ (𝑦 ∖ {∅}) → (𝑔‘𝑧) ∈ 𝑧))
32		impexp 439	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧) ↔ (𝑧 ∈ 𝑦 → (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)))
33	24, 31, 32	3bitr3i 292	. . . . . . . . . 10 ⊢ ((𝑧 ∈ (𝑦 ∖ {∅}) → (𝑔‘𝑧) ∈ 𝑧) ↔ (𝑧 ∈ 𝑦 → (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)))
34	33	ralbii2 3166	. . . . . . . . 9 ⊢ (∀𝑧 ∈ (𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧 ↔ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))
35	22, 34	sylib 209	. . . . . . . 8 ⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦 ∧ ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))
36		fvrn0 6436	. . . . . . . . . . 11 ⊢ (𝑔‘𝑥) ∈ (ran 𝑔 ∪ {∅})
37	36	rgenw 3112	. . . . . . . . . 10 ⊢ ∀𝑥 ∈ 𝑦 (𝑔‘𝑥) ∈ (ran 𝑔 ∪ {∅})
38	26	fmpt 6602	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑦 (𝑔‘𝑥) ∈ (ran 𝑔 ∪ {∅}) ↔ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)):𝑦⟶(ran 𝑔 ∪ {∅}))
39	37, 38	mpbi 221	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)):𝑦⟶(ran 𝑔 ∪ {∅})
40		ffn 6256	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)):𝑦⟶(ran 𝑔 ∪ {∅}) → (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦)
41	39, 40	ax-mp 5	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦
42	35, 41	jctil 511	. . . . . . 7 ⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦 ∧ ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)))
43		fneq1 6190	. . . . . . . . 9 ⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → (𝑓 Fn 𝑦 ↔ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦))
44		fveq1 6407	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → (𝑓‘𝑧) = ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧))
45	44	eleq1d 2870	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → ((𝑓‘𝑧) ∈ 𝑧 ↔ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))
46	45	imbi2d 331	. . . . . . . . . 10 ⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)))
47	46	ralbidv 3174	. . . . . . . . 9 ⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → (∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)))
48	43, 47	anbi12d 618	. . . . . . . 8 ⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → ((𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ↔ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))))
49	48	spcegv 3487	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) ∈ V → (((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))))
50	21, 42, 49	mpsyl 68	. . . . . 6 ⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦 ∧ ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
51	50	exlimiv 2021	. . . . 5 ⊢ (∃𝑔(𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦 ∧ ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
52	9, 20, 51	3syl 18	. . . 4 ⊢ (∀𝑥AC 𝑥 = V → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
53	52	alrimiv 2018	. . 3 ⊢ (∀𝑥AC 𝑥 = V → ∀𝑦∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
54		dfac4 9228	. . 3 ⊢ (CHOICE ↔ ∀𝑦∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
55	53, 54	sylibr 225	. 2 ⊢ (∀𝑥AC 𝑥 = V → CHOICE)
56	3, 55	impbii 200	1 ⊢ (CHOICE ↔ ∀𝑥AC 𝑥 = V)

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384  ∀wal 1635   = wceq 1637  ∃wex 1859   ∈ wcel 2156   ≠ wne 2978  ∀wral 3096  Vcvv 3391   ∖ cdif 3766   ∪ cun 3767   ⊆ wss 3769  ∅c0 4116  {csn 4370  ∪ cuni 4630   ↦ cmpt 4923  ran crn 5312   Fn wfn 6096  ⟶wf 6097  ‘cfv 6101  AC wacn 9047  CHOICEwac 9221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-er 7979  df-map 8094  df-en 8193  df-dom 8194  df-card 9048  df-acn 9051  df-ac 9222

This theorem is referenced by:  dfac13  9249