Theorem dfac8

Description: A proof of the equivalency of the well-ordering theorem weth and the axiom of choice ac7 . (Contributed by Mario Carneiro, 5-Jan-2013)

	Ref	Expression
Assertion	dfac8	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		dfac3	⊢ ( CHOICE ↔ ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
2		vex	⊢ 𝑥 ∈ V
3		vpwex	⊢ 𝒫 𝑥 ∈ V
4		raleq	⊢ ( 𝑦 = 𝒫 𝑥 → ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝒫 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
5	4	exbidv	⊢ ( 𝑦 = 𝒫 𝑥 → ( ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∃ 𝑓 ∀ 𝑧 ∈ 𝒫 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
6	3 5	spcv	⊢ ( ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝒫 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
7		dfac8a	⊢ ( 𝑥 ∈ V → ( ∃ 𝑓 ∀ 𝑧 ∈ 𝒫 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → 𝑥 ∈ dom card ) )
8	2 6 7	mpsyl	⊢ ( ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → 𝑥 ∈ dom card )
9		dfac8b	⊢ ( 𝑥 ∈ dom card → ∃ 𝑟 𝑟 We 𝑥 )
10	8 9	syl	⊢ ( ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑟 𝑟 We 𝑥 )
11	10	alrimiv	⊢ ( ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 )
12		vex	⊢ 𝑦 ∈ V
13		vuniex	⊢ ∪ 𝑦 ∈ V
14		weeq2	⊢ ( 𝑥 = ∪ 𝑦 → ( 𝑟 We 𝑥 ↔ 𝑟 We ∪ 𝑦 ) )
15	14	exbidv	⊢ ( 𝑥 = ∪ 𝑦 → ( ∃ 𝑟 𝑟 We 𝑥 ↔ ∃ 𝑟 𝑟 We ∪ 𝑦 ) )
16	13 15	spcv	⊢ ( ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 → ∃ 𝑟 𝑟 We ∪ 𝑦 )
17		dfac8c	⊢ ( 𝑦 ∈ V → ( ∃ 𝑟 𝑟 We ∪ 𝑦 → ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
18	12 16 17	mpsyl	⊢ ( ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 → ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
19	18	alrimiv	⊢ ( ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 → ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
20	11 19	impbii	⊢ ( ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 )
21	1 20	bitri	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 )