inaprc

Description: An equivalent to the Tarski-Grothendieck Axiom: there is a proper class of inaccessible cardinals. (Contributed by Mario Carneiro, 9-Jun-2013)

		Ref	Expression
	Assertion	inaprc	⊢ Inacc ∉ V

Proof

Step	Hyp	Ref	Expression
1		inawina	⊢ ( 𝑥 ∈ Inacc → 𝑥 ∈ Inacc_w )
2		winaon	⊢ ( 𝑥 ∈ Inacc_w → 𝑥 ∈ On )
3	1 2	syl	⊢ ( 𝑥 ∈ Inacc → 𝑥 ∈ On )
4	3	ssriv	⊢ Inacc ⊆ On
5		ssorduni	⊢ ( Inacc ⊆ On → Ord ∪ Inacc )
6		ordsson	⊢ ( Ord ∪ Inacc → ∪ Inacc ⊆ On )
7	4 5 6	mp2b	⊢ ∪ Inacc ⊆ On
8		vex	⊢ 𝑦 ∈ V
9		grothtsk	⊢ ∪ Tarski = V
10	8 9	eleqtrri	⊢ 𝑦 ∈ ∪ Tarski
11		eluni2	⊢ ( 𝑦 ∈ ∪ Tarski ↔ ∃ 𝑤 ∈ Tarski 𝑦 ∈ 𝑤 )
12	10 11	mpbi	⊢ ∃ 𝑤 ∈ Tarski 𝑦 ∈ 𝑤
13		ne0i	⊢ ( 𝑦 ∈ 𝑤 → 𝑤 ≠ ∅ )
14		tskcard	⊢ ( ( 𝑤 ∈ Tarski ∧ 𝑤 ≠ ∅ ) → ( card ‘ 𝑤 ) ∈ Inacc )
15	13 14	sylan2	⊢ ( ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) → ( card ‘ 𝑤 ) ∈ Inacc )
16		tsksdom	⊢ ( ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) → 𝑦 ≺ 𝑤 )
17	16	adantl	⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) ) → 𝑦 ≺ 𝑤 )
18		tskwe2	⊢ ( 𝑤 ∈ Tarski → 𝑤 ∈ dom card )
19	18	adantr	⊢ ( ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) → 𝑤 ∈ dom card )
20		cardsdomel	⊢ ( ( 𝑦 ∈ On ∧ 𝑤 ∈ dom card ) → ( 𝑦 ≺ 𝑤 ↔ 𝑦 ∈ ( card ‘ 𝑤 ) ) )
21	19 20	sylan2	⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) ) → ( 𝑦 ≺ 𝑤 ↔ 𝑦 ∈ ( card ‘ 𝑤 ) ) )
22	17 21	mpbid	⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) ) → 𝑦 ∈ ( card ‘ 𝑤 ) )
23		eleq2	⊢ ( 𝑧 = ( card ‘ 𝑤 ) → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ ( card ‘ 𝑤 ) ) )
24	23	rspcev	⊢ ( ( ( card ‘ 𝑤 ) ∈ Inacc ∧ 𝑦 ∈ ( card ‘ 𝑤 ) ) → ∃ 𝑧 ∈ Inacc 𝑦 ∈ 𝑧 )
25	15 22 24	syl2an2	⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) ) → ∃ 𝑧 ∈ Inacc 𝑦 ∈ 𝑧 )
26	25	rexlimdvaa	⊢ ( 𝑦 ∈ On → ( ∃ 𝑤 ∈ Tarski 𝑦 ∈ 𝑤 → ∃ 𝑧 ∈ Inacc 𝑦 ∈ 𝑧 ) )
27	12 26	mpi	⊢ ( 𝑦 ∈ On → ∃ 𝑧 ∈ Inacc 𝑦 ∈ 𝑧 )
28		eluni2	⊢ ( 𝑦 ∈ ∪ Inacc ↔ ∃ 𝑧 ∈ Inacc 𝑦 ∈ 𝑧 )
29	27 28	sylibr	⊢ ( 𝑦 ∈ On → 𝑦 ∈ ∪ Inacc )
30	29	ssriv	⊢ On ⊆ ∪ Inacc
31	7 30	eqssi	⊢ ∪ Inacc = On
32		ssonprc	⊢ ( Inacc ⊆ On → ( Inacc ∉ V ↔ ∪ Inacc = On ) )
33	4 32	ax-mp	⊢ ( Inacc ∉ V ↔ ∪ Inacc = On )
34	31 33	mpbir	⊢ Inacc ∉ V

Metamath Proof Explorer

Theorem inaprc

Proof