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		onss	⊢ ( 𝑦 ∈ On → 𝑦 ⊆ On )
4	3	a1i	⊢ ( 𝑓 : 𝐴 –1-1→ 𝑦 → ( 𝑦 ∈ On → 𝑦 ⊆ On ) )
5		epweon	⊢ E We On
6		wess	⊢ ( 𝑦 ⊆ On → ( E We On → E We 𝑦 ) )
7	4 5 6	syl6mpi	⊢ ( 𝑓 : 𝐴 –1-1→ 𝑦 → ( 𝑦 ∈ On → E We 𝑦 ) )
8	7	adantl	⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑓 : 𝐴 –1-1→ 𝑦 ) → ( 𝑦 ∈ On → E We 𝑦 ) )
9		eqid	⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) }
10	9	f1we	⊢ ( 𝑓 : 𝐴 –1-1→ 𝑦 → ( E We 𝑦 → { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } We 𝐴 ) )
11		weinxp	⊢ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } We 𝐴 ↔ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
12		reldom	⊢ Rel ≼
13	12	brrelex1i	⊢ ( 𝐴 ≼ 𝑦 → 𝐴 ∈ V )
14		sqxpexg	⊢ ( 𝐴 ∈ V → ( 𝐴 × 𝐴 ) ∈ V )
15		inex2g	⊢ ( ( 𝐴 × 𝐴 ) ∈ V → ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
16		weeq1	⊢ ( 𝑥 = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) → ( 𝑥 We 𝐴 ↔ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ) )
17	16	spcegv	⊢ ( ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
18	13 14 15 17	4syl	⊢ ( 𝐴 ≼ 𝑦 → ( ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
19	11 18	biimtrid	⊢ ( 𝐴 ≼ 𝑦 → ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) E ( 𝑓 ‘ 𝑧 ) } We 𝐴 → ∃ 𝑥 𝑥 We 𝐴 ) )
20	10 19	sylan9r	⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑓 : 𝐴 –1-1→ 𝑦 ) → ( E We 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) )
21	8 20	syld	⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑓 : 𝐴 –1-1→ 𝑦 ) → ( 𝑦 ∈ On → ∃ 𝑥 𝑥 We 𝐴 ) )
22	21	impancom	⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On ) → ( 𝑓 : 𝐴 –1-1→ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) )
23	22	exlimdv	⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On ) → ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) )
24	2 23	biimtrid	⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On ) → ( 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) )
25	24	ex	⊢ ( 𝐴 ≼ 𝑦 → ( 𝑦 ∈ On → ( 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) ) )
26	25	pm2.43b	⊢ ( 𝑦 ∈ On → ( 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) )
27	26	rexlimiv	⊢ ( ∃ 𝑦 ∈ On 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 )