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	$⊢ \exists y \in On A ≼ y \to \exists x x We A$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ y \in V$
2	1	brdom	$⊢ A ≼ y \leftrightarrow \exists f f : A \underset{1-1}{⟶} y$
3		f1f	$⊢ f : A \underset{1-1}{⟶} y \to f : A ⟶ y$
4	3	frnd	$⊢ f : A \underset{1-1}{⟶} y \to ran f \subseteq y$
5		onss	$⊢ y \in On \to y \subseteq On$
6		sstr2	$⊢ ran f \subseteq y \to (y \subseteq On \to ran f \subseteq On)$
7	4 5 6	syl2im	$⊢ f : A \underset{1-1}{⟶} y \to (y \in On \to ran f \subseteq On)$
8		epweon	$⊢ E We On$
9		wess	$⊢ ran f \subseteq On \to (E We On \to E We ran f)$
10	7 8 9	syl6mpi	$⊢ f : A \underset{1-1}{⟶} y \to (y \in On \to E We ran f)$
11	10	adantl	$⊢ (A ≼ y \land f : A \underset{1-1}{⟶} y) \to (y \in On \to E We ran f)$
12		f1f1orn	$⊢ f : A \underset{1-1}{⟶} y \to f : A \underset{1-1 onto}{⟶} ran f$
13		eqid	$⊢ \{⟨w, z⟩ \| f (w) E f (z)\} = \{⟨w, z⟩ \| f (w) E f (z)\}$
14	13	f1owe	$⊢ f : A \underset{1-1 onto}{⟶} ran f \to (E We ran f \to \{⟨w, z⟩ \| f (w) E f (z)\} We A)$
15	12 14	syl	$⊢ f : A \underset{1-1}{⟶} y \to (E We ran f \to \{⟨w, z⟩ \| f (w) E f (z)\} We A)$
16		weinxp	$⊢ \{⟨w, z⟩ \| f (w) E f (z)\} We A \leftrightarrow (\{⟨w, z⟩ \| f (w) E f (z)\} \cap (A \times A)) We A$
17		reldom	$⊢ Rel ≼$
18	17	brrelex1i	$⊢ A ≼ y \to A \in V$
19		sqxpexg	$⊢ A \in V \to A \times A \in V$
20		incom	$⊢ (A \times A) \cap \{⟨w, z⟩ \| f (w) E f (z)\} = \{⟨w, z⟩ \| f (w) E f (z)\} \cap (A \times A)$
21		inex1g	$⊢ A \times A \in V \to (A \times A) \cap \{⟨w, z⟩ \| f (w) E f (z)\} \in V$
22	20 21	eqeltrrid	$⊢ A \times A \in V \to \{⟨w, z⟩ \| f (w) E f (z)\} \cap (A \times A) \in V$
23		weeq1	$⊢ x = \{⟨w, z⟩ \| f (w) E f (z)\} \cap (A \times A) \to (x We A \leftrightarrow (\{⟨w, z⟩ \| f (w) E f (z)\} \cap (A \times A)) We A)$
24	23	spcegv	$⊢ \{⟨w, z⟩ \| f (w) E f (z)\} \cap (A \times A) \in V \to ((\{⟨w, z⟩ \| f (w) E f (z)\} \cap (A \times A)) We A \to \exists x x We A)$
25	18 19 22 24	4syl	$⊢ A ≼ y \to ((\{⟨w, z⟩ \| f (w) E f (z)\} \cap (A \times A)) We A \to \exists x x We A)$
26	16 25	biimtrid	$⊢ A ≼ y \to (\{⟨w, z⟩ \| f (w) E f (z)\} We A \to \exists x x We A)$
27	15 26	sylan9r	$⊢ (A ≼ y \land f : A \underset{1-1}{⟶} y) \to (E We ran f \to \exists x x We A)$
28	11 27	syld	$⊢ (A ≼ y \land f : A \underset{1-1}{⟶} y) \to (y \in On \to \exists x x We A)$
29	28	impancom	$⊢ (A ≼ y \land y \in On) \to (f : A \underset{1-1}{⟶} y \to \exists x x We A)$
30	29	exlimdv	$⊢ (A ≼ y \land y \in On) \to (\exists f f : A \underset{1-1}{⟶} y \to \exists x x We A)$
31	2 30	biimtrid	$⊢ (A ≼ y \land y \in On) \to (A ≼ y \to \exists x x We A)$
32	31	ex	$⊢ A ≼ y \to (y \in On \to (A ≼ y \to \exists x x We A))$
33	32	pm2.43b	$⊢ y \in On \to (A ≼ y \to \exists x x We A)$
34	33	rexlimiv	$⊢ \exists y \in On A ≼ y \to \exists x x We A$

Metamath Proof Explorer

Theorem ac10ct

Proof