Theorem dfac2a

Description: Our Axiom of Choice (in the form of ac3 ) implies the Axiom of Choice (first form) of Enderton p. 49. The proof uses neither AC nor the Axiom of Regularity. See dfac2b for the converse (which does use the Axiom of Regularity). (Contributed by NM, 5-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Assertion	dfac2a	⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → CHOICE )

Proof

Step	Hyp	Ref	Expression
1		riotauni	⊢ ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → ( ℩ 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) = ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } )
2		riotacl	⊢ ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → ( ℩ 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ∈ 𝑧 )
3	1 2	eqeltrrd	⊢ ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ 𝑧 )
4		elequ2	⊢ ( 𝑢 = 𝑧 → ( 𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑧 ) )
5		elequ1	⊢ ( 𝑢 = 𝑧 → ( 𝑢 ∈ 𝑣 ↔ 𝑧 ∈ 𝑣 ) )
6	5	anbi1d	⊢ ( 𝑢 = 𝑧 → ( ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
7	6	rexbidv	⊢ ( 𝑢 = 𝑧 → ( ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
8	4 7	anbi12d	⊢ ( 𝑢 = 𝑧 → ( ( 𝑤 ∈ 𝑢 ∧ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ↔ ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) )
9	8	rabbidva2	⊢ ( 𝑢 = 𝑧 → { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } = { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } )
10	9	unieqd	⊢ ( 𝑢 = 𝑧 → ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } = ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } )
11		eqid	⊢ ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) = ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } )
12		vex	⊢ 𝑧 ∈ V
13	12	rabex	⊢ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ V
14	13	uniex	⊢ ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ V
15	10 11 14	fvmpt	⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) = ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } )
16	15	eleq1d	⊢ ( 𝑧 ∈ 𝑥 → ( ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ↔ ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ 𝑧 ) )
17	3 16	imbitrrid	⊢ ( 𝑧 ∈ 𝑥 → ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) )
18	17	imim2d	⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ( 𝑧 ≠ ∅ → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
19	18	ralimia	⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) )
20		ssrab2	⊢ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ⊆ 𝑢
21		elssuni	⊢ ( 𝑢 ∈ 𝑥 → 𝑢 ⊆ ∪ 𝑥 )
22	20 21	sstrid	⊢ ( 𝑢 ∈ 𝑥 → { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ⊆ ∪ 𝑥 )
23	22	unissd	⊢ ( 𝑢 ∈ 𝑥 → ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ⊆ ∪ ∪ 𝑥 )
24		vex	⊢ 𝑥 ∈ V
25	24	uniex	⊢ ∪ 𝑥 ∈ V
26	25	uniex	⊢ ∪ ∪ 𝑥 ∈ V
27	26	elpw2	⊢ ( ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ 𝒫 ∪ ∪ 𝑥 ↔ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ⊆ ∪ ∪ 𝑥 )
28	23 27	sylibr	⊢ ( 𝑢 ∈ 𝑥 → ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ 𝒫 ∪ ∪ 𝑥 )
29	11 28	fmpti	⊢ ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) : 𝑥 ⟶ 𝒫 ∪ ∪ 𝑥
30	26	pwex	⊢ 𝒫 ∪ ∪ 𝑥 ∈ V
31		fex2	⊢ ( ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) : 𝑥 ⟶ 𝒫 ∪ ∪ 𝑥 ∧ 𝑥 ∈ V ∧ 𝒫 ∪ ∪ 𝑥 ∈ V ) → ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ∈ V )
32	29 24 30 31	mp3an	⊢ ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ∈ V
33		fveq1	⊢ ( 𝑓 = ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) → ( 𝑓 ‘ 𝑧 ) = ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) )
34	33	eleq1d	⊢ ( 𝑓 = ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) )
35	34	imbi2d	⊢ ( 𝑓 = ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
36	35	ralbidv	⊢ ( 𝑓 = ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
37	32 36	spcev	⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
38	19 37	syl	⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
39	38	exlimiv	⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
40	39	alimi	⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
41		dfac3	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
42	40 41	sylibr	⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → CHOICE )