Theorem untangtr

Description: A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011)

	Ref	Expression
Assertion	untangtr	⊢ ( Tr 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		df-tr	⊢ ( Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴 )
2		ssralv	⊢ ( ∪ 𝐴 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ) )
3	1 2	sylbi	⊢ ( Tr 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ) )
4		elequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
5		elequ2	⊢ ( 𝑥 = 𝑦 → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) )
6	4 5	bitrd	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) )
7	6	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝑦 ∈ 𝑦 ) )
8	7	cbvralvw	⊢ ( ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀ 𝑦 ∈ ∪ 𝐴 ¬ 𝑦 ∈ 𝑦 )
9		untuni	⊢ ( ∀ 𝑦 ∈ ∪ 𝐴 ¬ 𝑦 ∈ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 )
10	8 9	bitri	⊢ ( ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 )
11	3 10	syl6ib	⊢ ( Tr 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 ) )
12		untelirr	⊢ ( ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 )
13	12	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 )
14	11 13	impbid1	⊢ ( Tr 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 ) )