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

Metamath Proof Explorer

Theorem ac10ct

Description: A proof of the well-ordering theorem weth , an Axiom of Choice equivalent, restricted to sets dominated by some ordinal (in particular finite sets and countable sets), proven in ZF without AC. (Contributed by Mario Carneiro, 5-Jan-2013)

Ref Expression
Assertion ac10ct ( ∃ 𝑦 ∈ On 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑦 ∈ V
2 1 brdom ⊢ ( 𝐴 ≼ 𝑦 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝑦 )
3 f1f ⊢ ( 𝑓 : 𝐴 –1-1→ 𝑦 → 𝑓 : 𝐴 ⟶ 𝑦 )
4 3 frnd ⊢ ( 𝑓 : 𝐴 –1-1→ 𝑦 → ran 𝑓 ⊆ 𝑦 )
5 onss ⊢ ( 𝑦 ∈ On → 𝑦 ⊆ On )
6 sstr2 ⊢ ( ran 𝑓 ⊆ 𝑦 → ( 𝑦 ⊆ On → ran 𝑓 ⊆ On ) )
7 4 5 6 syl2im ⊢ ( 𝑓 : 𝐴 –1-1→ 𝑦 → ( 𝑦 ∈ On → ran 𝑓 ⊆ On ) )
8 epweon ⊢ E We On
9 wess ⊢ ( ran 𝑓 ⊆ On → ( E We On → E We ran 𝑓 ) )
10 7 8 9 syl6mpi ⊢ ( 𝑓 : 𝐴 –1-1→ 𝑦 → ( 𝑦 ∈ On → E We ran 𝑓 ) )
11 10 adantl ⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑓 : 𝐴 –1-1→ 𝑦 ) → ( 𝑦 ∈ On → E We ran 𝑓 ) )
12 f1f1orn ⊢ ( 𝑓 : 𝐴 –1-1→ 𝑦 → 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 )
13 eqid ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) }
14 13 f1owe ⊢ ( 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 → ( E We ran 𝑓 → { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } We 𝐴 ) )
15 12 14 syl ⊢ ( 𝑓 : 𝐴 –1-1→ 𝑦 → ( E We ran 𝑓 → { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } We 𝐴 ) )
16 weinxp ⊢ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } We 𝐴 ↔ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
17 reldom ⊢ Rel ≼
18 17 brrelex1i ⊢ ( 𝐴 ≼ 𝑦 → 𝐴 ∈ V )
19 sqxpexg ⊢ ( 𝐴 ∈ V → ( 𝐴 × 𝐴 ) ∈ V )
20 incom ⊢ ( ( 𝐴 × 𝐴 ) ∩ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ) = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) )
21 inex1g ⊢ ( ( 𝐴 × 𝐴 ) ∈ V → ( ( 𝐴 × 𝐴 ) ∩ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ) ∈ V )
22 20 21 eqeltrrid ⊢ ( ( 𝐴 × 𝐴 ) ∈ V → ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
23 weeq1 ⊢ ( 𝑥 = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) → ( 𝑥 We 𝐴 ↔ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ) )
24 23 spcegv ⊢ ( ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
25 18 19 22 24 4syl ⊢ ( 𝐴 ≼ 𝑦 → ( ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
26 16 25 biimtrid ⊢ ( 𝐴 ≼ 𝑦 → ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } We 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
27 15 26 sylan9r ⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑓 : 𝐴 –1-1→ 𝑦 ) → ( E We ran 𝑓 → ∃ 𝑥 𝑥 We 𝐴 ) )
28 11 27 syld ⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑓 : 𝐴 –1-1→ 𝑦 ) → ( 𝑦 ∈ On → ∃ 𝑥 𝑥 We 𝐴 ) )
29 28 impancom ⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On ) → ( 𝑓 : 𝐴 –1-1→ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) )
30 29 exlimdv ⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On ) → ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) )
31 2 30 biimtrid ⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On ) → ( 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) )
32 31 ex ⊢ ( 𝐴 ≼ 𝑦 → ( 𝑦 ∈ On → ( 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) ) )
33 32 pm2.43b ⊢ ( 𝑦 ∈ On → ( 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) )
34 33 rexlimiv ⊢ ( ∃ 𝑦 ∈ On 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 )