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	syl5bi	⊢ ( 𝐴 ≼ 𝑦 → ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑓 ‘ 𝑤 ) 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	syl5bi	⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On ) → ( 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) )
32	31	ex	⊢ ( 𝐴 ≼ 𝑦 → ( 𝑦 ∈ On → ( 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) ) )
33	32	pm2.43b	⊢ ( 𝑦 ∈ On → ( 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 ) )
34	33	rexlimiv	⊢ ( ∃ 𝑦 ∈ On 𝐴 ≼ 𝑦 → ∃ 𝑥 𝑥 We 𝐴 )