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	⊢ ( 𝐴 ∈ On → ∃ 𝑥 ∈ Inacc 𝐴 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		inawina	⊢ ( 𝑥 ∈ Inacc → 𝑥 ∈ Inaccw )
2		winaon	⊢ ( 𝑥 ∈ Inaccw → 𝑥 ∈ On )
3	1 2	syl	⊢ ( 𝑥 ∈ Inacc → 𝑥 ∈ On )
4	3	ssriv	⊢ Inacc ⊆ On
5		onmindif	⊢ ( ( Inacc ⊆ On ∧ 𝐴 ∈ On ) → 𝐴 ∈ ∩ ( Inacc ∖ suc 𝐴 ) )
6	4 5	mpan	⊢ ( 𝐴 ∈ On → 𝐴 ∈ ∩ ( Inacc ∖ suc 𝐴 ) )
7	6	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 = ∩ ( Inacc ∖ suc 𝐴 ) ) → 𝐴 ∈ ∩ ( Inacc ∖ suc 𝐴 ) )
8		simpr	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 = ∩ ( Inacc ∖ suc 𝐴 ) ) → 𝑥 = ∩ ( Inacc ∖ suc 𝐴 ) )
9	7 8	eleqtrrd	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 = ∩ ( Inacc ∖ suc 𝐴 ) ) → 𝐴 ∈ 𝑥 )
10		difss	⊢ ( Inacc ∖ suc 𝐴 ) ⊆ Inacc
11	10 4	sstri	⊢ ( Inacc ∖ suc 𝐴 ) ⊆ On
12		inaprc	⊢ Inacc ∉ V
13	12	neli	⊢ ¬ Inacc ∈ V
14		ssdif0	⊢ ( Inacc ⊆ suc 𝐴 ↔ ( Inacc ∖ suc 𝐴 ) = ∅ )
15		sucexg	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ V )
16		ssexg	⊢ ( ( Inacc ⊆ suc 𝐴 ∧ suc 𝐴 ∈ V ) → Inacc ∈ V )
17	16	expcom	⊢ ( suc 𝐴 ∈ V → ( Inacc ⊆ suc 𝐴 → Inacc ∈ V ) )
18	15 17	syl	⊢ ( 𝐴 ∈ On → ( Inacc ⊆ suc 𝐴 → Inacc ∈ V ) )
19	14 18	syl5bir	⊢ ( 𝐴 ∈ On → ( ( Inacc ∖ suc 𝐴 ) = ∅ → Inacc ∈ V ) )
20	13 19	mtoi	⊢ ( 𝐴 ∈ On → ¬ ( Inacc ∖ suc 𝐴 ) = ∅ )
21	20	neqned	⊢ ( 𝐴 ∈ On → ( Inacc ∖ suc 𝐴 ) ≠ ∅ )
22		onint	⊢ ( ( ( Inacc ∖ suc 𝐴 ) ⊆ On ∧ ( Inacc ∖ suc 𝐴 ) ≠ ∅ ) → ∩ ( Inacc ∖ suc 𝐴 ) ∈ ( Inacc ∖ suc 𝐴 ) )
23	11 21 22	sylancr	⊢ ( 𝐴 ∈ On → ∩ ( Inacc ∖ suc 𝐴 ) ∈ ( Inacc ∖ suc 𝐴 ) )
24	23	eldifad	⊢ ( 𝐴 ∈ On → ∩ ( Inacc ∖ suc 𝐴 ) ∈ Inacc )
25	9 24	rspcime	⊢ ( 𝐴 ∈ On → ∃ 𝑥 ∈ Inacc 𝐴 ∈ 𝑥 )