inaex

Description: Assuming the Tarski-Grothendieck axiom, every ordinal is contained in an inaccessible ordinal. (Contributed by Rohan Ridenour, 13-Aug-2023)

		Ref	Expression
	Assertion	inaex	$⊢ A \in On \to \exists x \in Inacc A \in x$

Proof

Step	Hyp	Ref	Expression
1		inawina	$⊢ x \in Inacc \to x \in {Inacc}_{𝑤}$
2		winaon	$⊢ x \in {Inacc}_{𝑤} \to x \in On$
3	1 2	syl	$⊢ x \in Inacc \to x \in On$
4	3	ssriv	$⊢ Inacc \subseteq On$
5		onmindif	$⊢ (Inacc \subseteq On \land A \in On) \to A \in ⋂ (Inacc ∖ suc A)$
6	4 5	mpan	$⊢ A \in On \to A \in ⋂ (Inacc ∖ suc A)$
7	6	adantr	$⊢ (A \in On \land x = ⋂ (Inacc ∖ suc A)) \to A \in ⋂ (Inacc ∖ suc A)$
8		simpr	$⊢ (A \in On \land x = ⋂ (Inacc ∖ suc A)) \to x = ⋂ (Inacc ∖ suc A)$
9	7 8	eleqtrrd	$⊢ (A \in On \land x = ⋂ (Inacc ∖ suc A)) \to A \in x$
10		difss	$⊢ Inacc ∖ suc A \subseteq Inacc$
11	10 4	sstri	$⊢ Inacc ∖ suc A \subseteq On$
12		inaprc	$⊢ Inacc \notin V$
13	12	neli	$⊢ \neg Inacc \in V$
14		ssdif0	$⊢ Inacc \subseteq suc A \leftrightarrow Inacc ∖ suc A = \emptyset$
15		sucexg	$⊢ A \in On \to suc A \in V$
16		ssexg	$⊢ (Inacc \subseteq suc A \land suc A \in V) \to Inacc \in V$
17	16	expcom	$⊢ suc A \in V \to (Inacc \subseteq suc A \to Inacc \in V)$
18	15 17	syl	$⊢ A \in On \to (Inacc \subseteq suc A \to Inacc \in V)$
19	14 18	biimtrrid	$⊢ A \in On \to (Inacc ∖ suc A = \emptyset \to Inacc \in V)$
20	13 19	mtoi	$⊢ A \in On \to \neg Inacc ∖ suc A = \emptyset$
21	20	neqned	$⊢ A \in On \to Inacc ∖ suc A \neq \emptyset$
22		onint	$⊢ (Inacc ∖ suc A \subseteq On \land Inacc ∖ suc A \neq \emptyset) \to ⋂ (Inacc ∖ suc A) \in (Inacc ∖ suc A)$
23	11 21 22	sylancr	$⊢ A \in On \to ⋂ (Inacc ∖ suc A) \in (Inacc ∖ suc A)$
24	23	eldifad	$⊢ A \in On \to ⋂ (Inacc ∖ suc A) \in Inacc$
25	9 24	rspcime	$⊢ A \in On \to \exists x \in Inacc A \in x$

Metamath Proof Explorer

Theorem inaex

Proof