Metamath Proof Explorer

Theorem dfac8b

Description: The well-ordering theorem: every numerable set is well-orderable. (Contributed by Mario Carneiro, 5-Jan-2013) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion dfac8b ( 𝐴 ∈ dom card → ∃ 𝑥 𝑥 We 𝐴 )

Proof

Step Hyp Ref Expression
1 cardid2 ⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
2 bren ⊢ ( ( card ‘ 𝐴 ) ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 )
3 1 2 sylib ⊢ ( 𝐴 ∈ dom card → ∃ 𝑓 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 )
4 sqxpexg ⊢ ( 𝐴 ∈ dom card → ( 𝐴 × 𝐴 ) ∈ V )
5 inex2g ⊢ ( ( 𝐴 × 𝐴 ) ∈ V → ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
6 4 5 syl ⊢ ( 𝐴 ∈ dom card → ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
7 f1ocnv ⊢ ( 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐴 –1-1-onto→ ( card ‘ 𝐴 ) )
8 cardon ⊢ ( card ‘ 𝐴 ) ∈ On
9 8 onordi ⊢ Ord ( card ‘ 𝐴 )
10 ordwe ⊢ ( Ord ( card ‘ 𝐴 ) → E We ( card ‘ 𝐴 ) )
11 9 10 ax-mp ⊢ E We ( card ‘ 𝐴 )
12 eqid ⊢ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) }
13 12 f1owe ⊢ ( ◡ 𝑓 : 𝐴 –1-1-onto→ ( card ‘ 𝐴 ) → ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } We 𝐴 ↔ E We ( card ‘ 𝐴 ) ) )
14 11 13 mpbiri ⊢ ( ◡ 𝑓 : 𝐴 –1-1-onto→ ( card ‘ 𝐴 ) → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } We 𝐴 )
15 7 14 syl ⊢ ( 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } We 𝐴 )
16 weinxp ⊢ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } We 𝐴 ↔ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
17 15 16 sylib ⊢ ( 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 → ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
18 weeq1 ⊢ ( 𝑥 = ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) → ( 𝑥 We 𝐴 ↔ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ) )
19 18 spcegv ⊢ ( ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
20 6 17 19 syl2im ⊢ ( 𝐴 ∈ dom card → ( 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
21 20 exlimdv ⊢ ( 𝐴 ∈ dom card → ( ∃ 𝑓 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
22 3 21 mpd ⊢ ( 𝐴 ∈ dom card → ∃ 𝑥 𝑥 We 𝐴 )