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 incom ⊢ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) = ( ( 𝐴 × 𝐴 ) ∩ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } )
6 inex1g ⊢ ( ( 𝐴 × 𝐴 ) ∈ V → ( ( 𝐴 × 𝐴 ) ∩ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ) ∈ V )
7 5 6 eqeltrid ⊢ ( ( 𝐴 × 𝐴 ) ∈ V → ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
8 4 7 syl ⊢ ( 𝐴 ∈ dom card → ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
9 f1ocnv ⊢ ( 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐴 –1-1-onto→ ( card ‘ 𝐴 ) )
10 cardon ⊢ ( card ‘ 𝐴 ) ∈ On
11 10 onordi ⊢ Ord ( card ‘ 𝐴 )
12 ordwe ⊢ ( Ord ( card ‘ 𝐴 ) → E We ( card ‘ 𝐴 ) )
13 11 12 ax-mp ⊢ E We ( card ‘ 𝐴 )
14 eqid ⊢ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) }
15 14 f1owe ⊢ ( ◡ 𝑓 : 𝐴 –1-1-onto→ ( card ‘ 𝐴 ) → ( E We ( card ‘ 𝐴 ) → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } We 𝐴 ) )
16 9 13 15 mpisyl ⊢ ( 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } We 𝐴 )
17 weinxp ⊢ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } We 𝐴 ↔ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
18 16 17 sylib ⊢ ( 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 → ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
19 weeq1 ⊢ ( 𝑥 = ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) → ( 𝑥 We 𝐴 ↔ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ) )
20 19 spcegv ⊢ ( ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ◡ 𝑓 ‘ 𝑧 ) E ( ◡ 𝑓 ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
21 8 18 20 syl2im ⊢ ( 𝐴 ∈ dom card → ( 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
22 21 exlimdv ⊢ ( 𝐴 ∈ dom card → ( ∃ 𝑓 𝑓 : ( card ‘ 𝐴 ) –1-1-onto→ 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
23 3 22 mpd ⊢ ( 𝐴 ∈ dom card → ∃ 𝑥 𝑥 We 𝐴 )