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

Metamath Proof Explorer

Theorem elwina

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

Ref Expression
Assertion elwina ( 𝐴 ∈ Inaccw ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ Inaccw → 𝐴 ∈ 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 rexeq ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑦 ∈ 𝑧 𝑥 ≺ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
11 10 raleqbi1dv ⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑧 𝑥 ≺ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
12 6 9 11 3anbi123d ⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 ≠ ∅ ∧ ( cf ‘ 𝑧 ) = 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑧 𝑥 ≺ 𝑦 ) ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ) )
13 df-wina ⊢ Inaccw = { 𝑧 ∣ ( 𝑧 ≠ ∅ ∧ ( cf ‘ 𝑧 ) = 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑧 𝑥 ≺ 𝑦 ) }
14 12 13 elab2g ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ Inaccw ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ) )
15 1 5 14 pm5.21nii ⊢ ( 𝐴 ∈ Inaccw ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )