Metamath Proof Explorer


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 𝑥 )