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 ⊢ Ⅎ 𝑦 𝐴
Assertion untsucf ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ∀ 𝑦 ∈ suc 𝐴 ¬ 𝑦 ∈ 𝑦 )

Proof

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