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