elina

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

		Ref	Expression
	Assertion	elina	$⊢ A \in Inacc \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A)$

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in Inacc \to A \in V$
2		fvex	$⊢ cf (A) \in V$
3		eleq1	$⊢ cf (A) = A \to (cf (A) \in V \leftrightarrow A \in V)$
4	2 3	mpbii	$⊢ cf (A) = A \to A \in V$
5	4	3ad2ant2	$⊢ (A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A) \to A \in V$
6		neeq1	$⊢ y = A \to (y \neq \emptyset \leftrightarrow A \neq \emptyset)$
7		fveq2	$⊢ y = A \to cf (y) = cf (A)$
8		eqeq12	$⊢ (cf (y) = cf (A) \land y = A) \to (cf (y) = y \leftrightarrow cf (A) = A)$
9	7 8	mpancom	$⊢ y = A \to (cf (y) = y \leftrightarrow cf (A) = A)$
10		breq2	$⊢ y = A \to (𝒫 x ≺ y \leftrightarrow 𝒫 x ≺ A)$
11	10	raleqbi1dv	$⊢ y = A \to (\forall x \in y 𝒫 x ≺ y \leftrightarrow \forall x \in A 𝒫 x ≺ A)$
12	6 9 11	3anbi123d	$⊢ y = A \to ((y \neq \emptyset \land cf (y) = y \land \forall x \in y 𝒫 x ≺ y) \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A))$
13		df-ina	$⊢ Inacc = \{y \| (y \neq \emptyset \land cf (y) = y \land \forall x \in y 𝒫 x ≺ y)\}$
14	12 13	elab2g	$⊢ A \in V \to (A \in Inacc \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A))$
15	1 5 14	pm5.21nii	$⊢ A \in Inacc \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A)$

Metamath Proof Explorer