Theorem 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 e. On -> E. x e. Inacc A e. x )

Proof

Step	Hyp	Ref	Expression
1		inawina	|- ( x e. Inacc -> x e. InaccW )
2		winaon	|- ( x e. InaccW -> x e. On )
3	1 2	syl	|- ( x e. Inacc -> x e. On )
4	3	ssriv	|- Inacc C_ On
5		onmindif	|- ( ( Inacc C_ On /\ A e. On ) -> A e. |^| ( Inacc \ suc A ) )
6	4 5	mpan	|- ( A e. On -> A e. |^| ( Inacc \ suc A ) )
7	6	adantr	|- ( ( A e. On /\ x = |^| ( Inacc \ suc A ) ) -> A e. |^| ( Inacc \ suc A ) )
8		simpr	|- ( ( A e. On /\ x = |^| ( Inacc \ suc A ) ) -> x = |^| ( Inacc \ suc A ) )
9	7 8	eleqtrrd	|- ( ( A e. On /\ x = |^| ( Inacc \ suc A ) ) -> A e. x )
10		difss	|- ( Inacc \ suc A ) C_ Inacc
11	10 4	sstri	|- ( Inacc \ suc A ) C_ On
12		inaprc	|- Inacc e/ _V
13	12	neli	|- -. Inacc e. _V
14		ssdif0	|- ( Inacc C_ suc A <-> ( Inacc \ suc A ) = (/) )
15		sucexg	|- ( A e. On -> suc A e. _V )
16		ssexg	|- ( ( Inacc C_ suc A /\ suc A e. _V ) -> Inacc e. _V )
17	16	expcom	|- ( suc A e. _V -> ( Inacc C_ suc A -> Inacc e. _V ) )
18	15 17	syl	|- ( A e. On -> ( Inacc C_ suc A -> Inacc e. _V ) )
19	14 18	syl5bir	|- ( A e. On -> ( ( Inacc \ suc A ) = (/) -> Inacc e. _V ) )
20	13 19	mtoi	|- ( A e. On -> -. ( Inacc \ suc A ) = (/) )
21	20	neqned	|- ( A e. On -> ( Inacc \ suc A ) =/= (/) )
22		onint	|- ( ( ( Inacc \ suc A ) C_ On /\ ( Inacc \ suc A ) =/= (/) ) -> |^| ( Inacc \ suc A ) e. ( Inacc \ suc A ) )
23	11 21 22	sylancr	|- ( A e. On -> |^| ( Inacc \ suc A ) e. ( Inacc \ suc A ) )
24	23	eldifad	|- ( A e. On -> |^| ( Inacc \ suc A ) e. Inacc )
25	9 24	rspcime	|- ( A e. On -> E. x e. Inacc A e. x )