This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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