This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elina

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

Ref Expression
Assertion elina ⊢ A ∈ Inacc ↔ A ≠ ∅ ∧ cf ⁡ A = A ∧ ∀ x ∈ A 𝒫 x ≺ A

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ Inacc → A ∈ V
2 fvex ⊢ cf ⁡ A ∈ V
3 eleq1 ⊢ cf ⁡ A = A → cf ⁡ A ∈ V ↔ A ∈ V
4 2 3 mpbii ⊢ cf ⁡ A = A → A ∈ V
5 4 3ad2ant2 ⊢ A ≠ ∅ ∧ cf ⁡ A = A ∧ ∀ x ∈ A 𝒫 x ≺ A → A ∈ V
6 neeq1 ⊢ y = A → y ≠ ∅ ↔ A ≠ ∅
7 fveq2 ⊢ y = A → cf ⁡ y = cf ⁡ A
8 eqeq12 ⊢ cf ⁡ y = cf ⁡ A ∧ y = A → cf ⁡ y = y ↔ cf ⁡ A = A
9 7 8 mpancom ⊢ y = A → cf ⁡ y = y ↔ cf ⁡ A = A
10 breq2 ⊢ y = A → 𝒫 x ≺ y ↔ 𝒫 x ≺ A
11 10 raleqbi1dv ⊢ y = A → ∀ x ∈ y 𝒫 x ≺ y ↔ ∀ x ∈ A 𝒫 x ≺ A
12 6 9 11 3anbi123d ⊢ y = A → y ≠ ∅ ∧ cf ⁡ y = y ∧ ∀ x ∈ y 𝒫 x ≺ y ↔ A ≠ ∅ ∧ cf ⁡ A = A ∧ ∀ x ∈ A 𝒫 x ≺ A
13 df-ina ⊢ Inacc = y | y ≠ ∅ ∧ cf ⁡ y = y ∧ ∀ x ∈ y 𝒫 x ≺ y
14 12 13 elab2g ⊢ A ∈ V → A ∈ Inacc ↔ A ≠ ∅ ∧ cf ⁡ A = A ∧ ∀ x ∈ A 𝒫 x ≺ A
15 1 5 14 pm5.21nii ⊢ A ∈ Inacc ↔ A ≠ ∅ ∧ cf ⁡ A = A ∧ ∀ x ∈ A 𝒫 x ≺ A