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	syl5bi	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ( 𝑦 ∈ suc 𝐴 → ¬ 𝑦 ∈ 𝑦 ) )
19	3 18	ralrimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ∀ 𝑦 ∈ suc 𝐴 ¬ 𝑦 ∈ 𝑦 )