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

Metamath Proof Explorer

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 imbitrdi ⊢ ( Tr 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 ) )
12 untelirr ⊢ ( ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 )
13 12 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 )
14 11 13 impbid1 ⊢ ( Tr 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 ) )