Metamath Proof Explorer

Theorem elwina

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

Ref Expression
Assertion elwina ⊢ A ∈ Inacc 𝑤 ↔ A ≠ ∅ ∧ cf ⁡ A = A ∧ ∀ x ∈ A ∃ y ∈ A x ≺ y

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 ∃ y ∈ A x ≺ y → A ∈ V
6 neeq1 ⊢ z = A → z ≠ ∅ ↔ A ≠ ∅
7 fveq2 ⊢ z = A → cf ⁡ z = cf ⁡ A
8 eqeq12 ⊢ cf ⁡ z = cf ⁡ A ∧ z = A → cf ⁡ z = z ↔ cf ⁡ A = A
9 7 8 mpancom ⊢ z = A → cf ⁡ z = z ↔ cf ⁡ A = A
10 rexeq ⊢ z = A → ∃ y ∈ z x ≺ y ↔ ∃ y ∈ A x ≺ y
11 10 raleqbi1dv ⊢ z = A → ∀ x ∈ z ∃ y ∈ z x ≺ y ↔ ∀ x ∈ A ∃ y ∈ A x ≺ y
12 6 9 11 3anbi123d ⊢ z = A → z ≠ ∅ ∧ cf ⁡ z = z ∧ ∀ x ∈ z ∃ y ∈ z x ≺ y ↔ A ≠ ∅ ∧ cf ⁡ A = A ∧ ∀ x ∈ A ∃ y ∈ A x ≺ y
13 df-wina ⊢ Inacc 𝑤 = z | z ≠ ∅ ∧ cf ⁡ z = z ∧ ∀ x ∈ z ∃ y ∈ z x ≺ y
14 12 13 elab2g ⊢ A ∈ V → A ∈ Inacc 𝑤 ↔ A ≠ ∅ ∧ cf ⁡ A = A ∧ ∀ x ∈ A ∃ y ∈ A x ≺ y
15 1 5 14 pm5.21nii ⊢ A ∈ Inacc 𝑤 ↔ A ≠ ∅ ∧ cf ⁡ A = A ∧ ∀ x ∈ A ∃ y ∈ A x ≺ y