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

Metamath Proof Explorer

Theorem untsucf

Description: If a class is untangled, then so is its successor. (Contributed by Scott Fenton, 28-Feb-2011) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypothesis untsucf.1 ⊢ Ⅎ _ y A
Assertion untsucf ⊢ ∀ x ∈ A ¬ x ∈ x → ∀ y ∈ suc ⁡ A ¬ y ∈ y

Proof

Step Hyp Ref Expression
1 untsucf.1 ⊢ Ⅎ _ y A
2 nfv ⊢ Ⅎ y ¬ x ∈ x
3 1 2 nfralw ⊢ Ⅎ y ∀ x ∈ A ¬ x ∈ x
4 vex ⊢ y ∈ V
5 4 elsuc ⊢ y ∈ suc ⁡ A ↔ y ∈ A ∨ y = A
6 elequ1 ⊢ x = y → x ∈ x ↔ y ∈ x
7 elequ2 ⊢ x = y → y ∈ x ↔ y ∈ y
8 6 7 bitrd ⊢ x = y → x ∈ x ↔ y ∈ y
9 8 notbid ⊢ x = y → ¬ x ∈ x ↔ ¬ y ∈ y
10 9 rspccv ⊢ ∀ x ∈ A ¬ x ∈ x → y ∈ A → ¬ y ∈ y
11 untelirr ⊢ ∀ x ∈ A ¬ x ∈ x → ¬ A ∈ A
12 eleq1 ⊢ y = A → y ∈ y ↔ A ∈ y
13 eleq2 ⊢ y = A → A ∈ y ↔ A ∈ A
14 12 13 bitrd ⊢ y = A → y ∈ y ↔ A ∈ A
15 14 notbid ⊢ y = A → ¬ y ∈ y ↔ ¬ A ∈ A
16 11 15 syl5ibrcom ⊢ ∀ x ∈ A ¬ x ∈ x → y = A → ¬ y ∈ y
17 10 16 jaod ⊢ ∀ x ∈ A ¬ x ∈ x → y ∈ A ∨ y = A → ¬ y ∈ y
18 5 17 biimtrid ⊢ ∀ x ∈ A ¬ x ∈ x → y ∈ suc ⁡ A → ¬ y ∈ y
19 3 18 ralrimi ⊢ ∀ x ∈ A ¬ x ∈ x → ∀ y ∈ suc ⁡ A ¬ y ∈ y