Theorem elina 10471

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

Assertion

Ref	Expression
elina	⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴))

Distinct variable group:   𝑥,𝐴

Proof of Theorem elina

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3452	. 2 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ V)
2		fvex 6805	. . . 4 ⊢ (cf‘𝐴) ∈ V
3		eleq1 2821	. . . 4 ⊢ ((cf‘𝐴) = 𝐴 → ((cf‘𝐴) ∈ V ↔ 𝐴 ∈ V))
4	2, 3	mpbii 232	. . 3 ⊢ ((cf‘𝐴) = 𝐴 → 𝐴 ∈ V)
5	4	3ad2ant2 1132	. 2 ⊢ ((𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴) → 𝐴 ∈ V)
6		neeq1 3001	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ≠ ∅ ↔ 𝐴 ≠ ∅))
7		fveq2 6792	. . . . 5 ⊢ (𝑦 = 𝐴 → (cf‘𝑦) = (cf‘𝐴))
8		eqeq12 2750	. . . . 5 ⊢ (((cf‘𝑦) = (cf‘𝐴) ∧ 𝑦 = 𝐴) → ((cf‘𝑦) = 𝑦 ↔ (cf‘𝐴) = 𝐴))
9	7, 8	mpancom 684	. . . 4 ⊢ (𝑦 = 𝐴 → ((cf‘𝑦) = 𝑦 ↔ (cf‘𝐴) = 𝐴))
10		breq2 5081	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝒫 𝑥 ≺ 𝑦 ↔ 𝒫 𝑥 ≺ 𝐴))
11	10	raleqbi1dv 3342	. . . 4 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝑦 𝒫 𝑥 ≺ 𝑦 ↔ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴))
12	6, 9, 11	3anbi123d 1434	. . 3 ⊢ (𝑦 = 𝐴 → ((𝑦 ≠ ∅ ∧ (cf‘𝑦) = 𝑦 ∧ ∀𝑥 ∈ 𝑦 𝒫 𝑥 ≺ 𝑦) ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴)))
13		df-ina 10469	. . 3 ⊢ Inacc = {𝑦 ∣ (𝑦 ≠ ∅ ∧ (cf‘𝑦) = 𝑦 ∧ ∀𝑥 ∈ 𝑦 𝒫 𝑥 ≺ 𝑦)}
14	12, 13	elab2g 3613	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴)))
15	1, 5, 14	pm5.21nii 379	1 ⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴))

Syntax hints:   ↔ wb 205   ∧ w3a 1085   = wceq 1537   ∈ wcel 2101   ≠ wne 2938  ∀wral 3059  Vcvv 3434  ∅c0 4259  𝒫 cpw 4536   class class class wbr 5077  ‘cfv 6447   ≺ csdm 8752  cfccf 9723  Inacccina 10467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-ext 2704  ax-nul 5233

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2939  df-ral 3060  df-rab 3224  df-v 3436  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4260  df-if 4463  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-br 5078  df-iota 6399  df-fv 6455  df-ina 10469

This theorem is referenced by:  inawina  10474  omina  10475  gchina  10483  inar1  10559  inatsk  10562  tskcard  10565  tskuni  10567  gruina  10602  grur1  10604