Theorem elina

Description: Conditions of strong inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013)

	Ref	Expression
Assertion	elina	⊢ ( 𝐴 ∈ Inacc ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ V )
2		fvex	⊢ ( cf ‘ 𝐴 ) ∈ V
3		eleq1	⊢ ( ( cf ‘ 𝐴 ) = 𝐴 → ( ( cf ‘ 𝐴 ) ∈ V ↔ 𝐴 ∈ V ) )
4	2 3	mpbii	⊢ ( ( cf ‘ 𝐴 ) = 𝐴 → 𝐴 ∈ V )
5	4	3ad2ant2	⊢ ( ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) → 𝐴 ∈ V )
6		neeq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ≠ ∅ ↔ 𝐴 ≠ ∅ ) )
7		fveq2	⊢ ( 𝑦 = 𝐴 → ( cf ‘ 𝑦 ) = ( cf ‘ 𝐴 ) )
8		eqeq12	⊢ ( ( ( cf ‘ 𝑦 ) = ( cf ‘ 𝐴 ) ∧ 𝑦 = 𝐴 ) → ( ( cf ‘ 𝑦 ) = 𝑦 ↔ ( cf ‘ 𝐴 ) = 𝐴 ) )
9	7 8	mpancom	⊢ ( 𝑦 = 𝐴 → ( ( cf ‘ 𝑦 ) = 𝑦 ↔ ( cf ‘ 𝐴 ) = 𝐴 ) )
10		breq2	⊢ ( 𝑦 = 𝐴 → ( 𝒫 𝑥 ≺ 𝑦 ↔ 𝒫 𝑥 ≺ 𝐴 ) )
11	10	raleqbi1dv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝑦 𝒫 𝑥 ≺ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) )
12	6 9 11	3anbi123d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ≠ ∅ ∧ ( cf ‘ 𝑦 ) = 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 𝒫 𝑥 ≺ 𝑦 ) ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) ) )
13		df-ina	⊢ Inacc = { 𝑦 ∣ ( 𝑦 ≠ ∅ ∧ ( cf ‘ 𝑦 ) = 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 𝒫 𝑥 ≺ 𝑦 ) }
14	12 13	elab2g	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ Inacc ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) ) )
15	1 5 14	pm5.21nii	⊢ ( 𝐴 ∈ Inacc ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) )