Metamath Proof Explorer


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 On x Inacc A x

Proof

Step Hyp Ref Expression
1 inawina x Inacc x Inacc 𝑤
2 winaon x Inacc 𝑤 x On
3 1 2 syl x Inacc x On
4 3 ssriv Inacc On
5 onmindif Inacc On A On A Inacc suc A
6 4 5 mpan A On A Inacc suc A
7 6 adantr A On x = Inacc suc A A Inacc suc A
8 simpr A On x = Inacc suc A x = Inacc suc A
9 7 8 eleqtrrd A On x = Inacc suc A A x
10 difss Inacc suc A Inacc
11 10 4 sstri Inacc suc A On
12 inaprc Inacc V
13 12 neli ¬ Inacc V
14 ssdif0 Inacc suc A Inacc suc A =
15 sucexg A On suc A V
16 ssexg Inacc suc A suc A V Inacc V
17 16 expcom suc A V Inacc suc A Inacc V
18 15 17 syl A On Inacc suc A Inacc V
19 14 18 syl5bir A On Inacc suc A = Inacc V
20 13 19 mtoi A On ¬ Inacc suc A =
21 20 neqned A On Inacc suc A
22 onint Inacc suc A On Inacc suc A Inacc suc A Inacc suc A
23 11 21 22 sylancr A On Inacc suc A Inacc suc A
24 23 eldifad A On Inacc suc A Inacc
25 9 24 rspcime A On x Inacc A x