Theorem 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 https://fomarchive.ugent.be/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	⊢ ( 𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦 )
2	1	sseq1d	⊢ ( 𝑥 = 𝑦 → ( 𝒫 𝑥 ⊆ 𝑢 ↔ 𝒫 𝑦 ⊆ 𝑢 ) )
3	1	eleq1d	⊢ ( 𝑥 = 𝑦 → ( 𝒫 𝑥 ∈ 𝑢 ↔ 𝒫 𝑦 ∈ 𝑢 ) )
4	2 3	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ↔ ( 𝒫 𝑦 ⊆ 𝑢 ∧ 𝒫 𝑦 ∈ 𝑢 ) ) )
5	4	rspcva	⊢ ( ( 𝑦 ∈ 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ) → ( 𝒫 𝑦 ⊆ 𝑢 ∧ 𝒫 𝑦 ∈ 𝑢 ) )
6	5	simpld	⊢ ( ( 𝑦 ∈ 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ) → 𝒫 𝑦 ⊆ 𝑢 )
7		rabss	⊢ ( { 𝑥 ∈ 𝒫 𝑢 ∣ 𝑥 ≺ 𝑢 } ⊆ 𝑢 ↔ ∀ 𝑥 ∈ 𝒫 𝑢 ( 𝑥 ≺ 𝑢 → 𝑥 ∈ 𝑢 ) )
8	7	biimpri	⊢ ( ∀ 𝑥 ∈ 𝒫 𝑢 ( 𝑥 ≺ 𝑢 → 𝑥 ∈ 𝑢 ) → { 𝑥 ∈ 𝒫 𝑢 ∣ 𝑥 ≺ 𝑢 } ⊆ 𝑢 )
9		vex	⊢ 𝑦 ∈ V
10	9	canth2	⊢ 𝑦 ≺ 𝒫 𝑦
11		sdomdom	⊢ ( 𝑦 ≺ 𝒫 𝑦 → 𝑦 ≼ 𝒫 𝑦 )
12	10 11	ax-mp	⊢ 𝑦 ≼ 𝒫 𝑦
13		ssdomg	⊢ ( 𝑢 ∈ V → ( 𝒫 𝑦 ⊆ 𝑢 → 𝒫 𝑦 ≼ 𝑢 ) )
14	13	elv	⊢ ( 𝒫 𝑦 ⊆ 𝑢 → 𝒫 𝑦 ≼ 𝑢 )
15		domtr	⊢ ( ( 𝑦 ≼ 𝒫 𝑦 ∧ 𝒫 𝑦 ≼ 𝑢 ) → 𝑦 ≼ 𝑢 )
16	12 14 15	sylancr	⊢ ( 𝒫 𝑦 ⊆ 𝑢 → 𝑦 ≼ 𝑢 )
17		vex	⊢ 𝑢 ∈ V
18		tskwe	⊢ ( ( 𝑢 ∈ V ∧ { 𝑥 ∈ 𝒫 𝑢 ∣ 𝑥 ≺ 𝑢 } ⊆ 𝑢 ) → 𝑢 ∈ dom card )
19	17 18	mpan	⊢ ( { 𝑥 ∈ 𝒫 𝑢 ∣ 𝑥 ≺ 𝑢 } ⊆ 𝑢 → 𝑢 ∈ dom card )
20		numdom	⊢ ( ( 𝑢 ∈ dom card ∧ 𝑦 ≼ 𝑢 ) → 𝑦 ∈ dom card )
21	20	expcom	⊢ ( 𝑦 ≼ 𝑢 → ( 𝑢 ∈ dom card → 𝑦 ∈ dom card ) )
22	16 19 21	syl2im	⊢ ( 𝒫 𝑦 ⊆ 𝑢 → ( { 𝑥 ∈ 𝒫 𝑢 ∣ 𝑥 ≺ 𝑢 } ⊆ 𝑢 → 𝑦 ∈ dom card ) )
23	6 8 22	syl2im	⊢ ( ( 𝑦 ∈ 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ) → ( ∀ 𝑥 ∈ 𝒫 𝑢 ( 𝑥 ≺ 𝑢 → 𝑥 ∈ 𝑢 ) → 𝑦 ∈ dom card ) )
24	23	3impia	⊢ ( ( 𝑦 ∈ 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑢 ( 𝑥 ≺ 𝑢 → 𝑥 ∈ 𝑢 ) ) → 𝑦 ∈ dom card )
25		axgroth6	⊢ ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑢 ( 𝑥 ≺ 𝑢 → 𝑥 ∈ 𝑢 ) )
26	24 25	exlimiiv	⊢ 𝑦 ∈ dom card
27	26 9	2th	⊢ ( 𝑦 ∈ dom card ↔ 𝑦 ∈ V )
28	27	eqriv	⊢ dom card = V