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 ⁡ A → ∀ x ∈ A ¬ x ∈ x ↔ ∀ x ∈ A ∀ y ∈ x ¬ y ∈ y

Proof

Step Hyp Ref Expression
1 df-tr ⊢ Tr ⁡ A ↔ ⋃ A ⊆ A
2 ssralv ⊢ ⋃ A ⊆ A → ∀ x ∈ A ¬ x ∈ x → ∀ x ∈ ⋃ A ¬ x ∈ x
3 1 2 sylbi ⊢ Tr ⁡ A → ∀ x ∈ A ¬ x ∈ x → ∀ x ∈ ⋃ A ¬ x ∈ x
4 elequ1 ⊢ x = y → x ∈ x ↔ y ∈ x
5 elequ2 ⊢ x = y → y ∈ x ↔ y ∈ y
6 4 5 bitrd ⊢ x = y → x ∈ x ↔ y ∈ y
7 6 notbid ⊢ x = y → ¬ x ∈ x ↔ ¬ y ∈ y
8 7 cbvralvw ⊢ ∀ x ∈ ⋃ A ¬ x ∈ x ↔ ∀ y ∈ ⋃ A ¬ y ∈ y
9 untuni ⊢ ∀ y ∈ ⋃ A ¬ y ∈ y ↔ ∀ x ∈ A ∀ y ∈ x ¬ y ∈ y
10 8 9 bitri ⊢ ∀ x ∈ ⋃ A ¬ x ∈ x ↔ ∀ x ∈ A ∀ y ∈ x ¬ y ∈ y
11 3 10 imbitrdi ⊢ Tr ⁡ A → ∀ x ∈ A ¬ x ∈ x → ∀ x ∈ A ∀ y ∈ x ¬ y ∈ y
12 untelirr ⊢ ∀ y ∈ x ¬ y ∈ y → ¬ x ∈ x
13 12 ralimi ⊢ ∀ x ∈ A ∀ y ∈ x ¬ y ∈ y → ∀ x ∈ A ¬ x ∈ x
14 11 13 impbid1 ⊢ Tr ⁡ A → ∀ x ∈ A ¬ x ∈ x ↔ ∀ x ∈ A ∀ y ∈ x ¬ y ∈ y