grothac

Description: The Tarski-Grothendieck Axiom implies the Axiom of Choice (in the form of cardeqv ). This can be put in a more conventional form via ween and dfac8 . Note that the mere existence of strongly inaccessible cardinals doesn't imply AC, but rather the particular form of the Tarski-Grothendieck axiom (see http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html ). (Contributed by Mario Carneiro, 19-Apr-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	grothac	$⊢ dom card = V$

Proof

Step	Hyp	Ref	Expression
1		pweq	$⊢ x = y \to 𝒫 x = 𝒫 y$
2	1	sseq1d	$⊢ x = y \to (𝒫 x \subseteq u \leftrightarrow 𝒫 y \subseteq u)$
3	1	eleq1d	$⊢ x = y \to (𝒫 x \in u \leftrightarrow 𝒫 y \in u)$
4	2 3	anbi12d	$⊢ x = y \to ((𝒫 x \subseteq u \land 𝒫 x \in u) \leftrightarrow (𝒫 y \subseteq u \land 𝒫 y \in u))$
5	4	rspcva	$⊢ (y \in u \land \forall x \in u (𝒫 x \subseteq u \land 𝒫 x \in u)) \to (𝒫 y \subseteq u \land 𝒫 y \in u)$
6	5	simpld	$⊢ (y \in u \land \forall x \in u (𝒫 x \subseteq u \land 𝒫 x \in u)) \to 𝒫 y \subseteq u$
7		rabss	$⊢ \{x \in 𝒫 u \| x ≺ u\} \subseteq u \leftrightarrow \forall x \in 𝒫 u (x ≺ u \to x \in u)$
8	7	biimpri	$⊢ \forall x \in 𝒫 u (x ≺ u \to x \in u) \to \{x \in 𝒫 u \| x ≺ u\} \subseteq u$
9		vex	$⊢ y \in V$
10	9	canth2	$⊢ y ≺ 𝒫 y$
11		sdomdom	$⊢ y ≺ 𝒫 y \to y ≼ 𝒫 y$
12	10 11	ax-mp	$⊢ y ≼ 𝒫 y$
13		ssdomg	$⊢ u \in V \to (𝒫 y \subseteq u \to 𝒫 y ≼ u)$
14	13	elv	$⊢ 𝒫 y \subseteq u \to 𝒫 y ≼ u$
15		domtr	$⊢ (y ≼ 𝒫 y \land 𝒫 y ≼ u) \to y ≼ u$
16	12 14 15	sylancr	$⊢ 𝒫 y \subseteq u \to y ≼ u$
17		vex	$⊢ u \in V$
18		tskwe	$⊢ (u \in V \land \{x \in 𝒫 u \| x ≺ u\} \subseteq u) \to u \in dom card$
19	17 18	mpan	$⊢ \{x \in 𝒫 u \| x ≺ u\} \subseteq u \to u \in dom card$
20		numdom	$⊢ (u \in dom card \land y ≼ u) \to y \in dom card$
21	20	expcom	$⊢ y ≼ u \to (u \in dom card \to y \in dom card)$
22	16 19 21	syl2im	$⊢ 𝒫 y \subseteq u \to (\{x \in 𝒫 u \| x ≺ u\} \subseteq u \to y \in dom card)$
23	6 8 22	syl2im	$⊢ (y \in u \land \forall x \in u (𝒫 x \subseteq u \land 𝒫 x \in u)) \to (\forall x \in 𝒫 u (x ≺ u \to x \in u) \to y \in dom card)$
24	23	3impia	$⊢ (y \in u \land \forall x \in u (𝒫 x \subseteq u \land 𝒫 x \in u) \land \forall x \in 𝒫 u (x ≺ u \to x \in u)) \to y \in dom card$
25		axgroth6	$⊢ \exists u (y \in u \land \forall x \in u (𝒫 x \subseteq u \land 𝒫 x \in u) \land \forall x \in 𝒫 u (x ≺ u \to x \in u))$
26	24 25	exlimiiv	$⊢ y \in dom card$
27	26 9	2th	$⊢ y \in dom card \leftrightarrow y \in V$
28	27	eqriv	$⊢ dom card = V$

Metamath Proof Explorer

Theorem grothac

Proof