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 ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )