Metamath Proof Explorer

Theorem dftr6

Description: A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012)

Ref Expression
Hypothesis dftr6.1 ⊢ A ∈ V
Assertion dftr6 ⊢ Tr ⁡ A ↔ A ∈ V ∖ ran ⁡ E ∘ E ∖ E

Proof

Step Hyp Ref Expression
1 dftr6.1 ⊢ A ∈ V
2 1 elrn ⊢ A ∈ ran ⁡ E ∘ E ∖ E ↔ ∃ x x E ∘ E ∖ E A
3 brdif ⊢ x E ∘ E ∖ E A ↔ x E ∘ E A ∧ ¬ x E A
4 vex ⊢ x ∈ V
5 4 1 brco ⊢ x E ∘ E A ↔ ∃ y x E y ∧ y E A
6 epel ⊢ x E y ↔ x ∈ y
7 1 epeli ⊢ y E A ↔ y ∈ A
8 6 7 anbi12i ⊢ x E y ∧ y E A ↔ x ∈ y ∧ y ∈ A
9 8 exbii ⊢ ∃ y x E y ∧ y E A ↔ ∃ y x ∈ y ∧ y ∈ A
10 5 9 bitri ⊢ x E ∘ E A ↔ ∃ y x ∈ y ∧ y ∈ A
11 1 epeli ⊢ x E A ↔ x ∈ A
12 11 notbii ⊢ ¬ x E A ↔ ¬ x ∈ A
13 10 12 anbi12i ⊢ x E ∘ E A ∧ ¬ x E A ↔ ∃ y x ∈ y ∧ y ∈ A ∧ ¬ x ∈ A
14 19.41v ⊢ ∃ y x ∈ y ∧ y ∈ A ∧ ¬ x ∈ A ↔ ∃ y x ∈ y ∧ y ∈ A ∧ ¬ x ∈ A
15 exanali ⊢ ∃ y x ∈ y ∧ y ∈ A ∧ ¬ x ∈ A ↔ ¬ ∀ y x ∈ y ∧ y ∈ A → x ∈ A
16 14 15 bitr3i ⊢ ∃ y x ∈ y ∧ y ∈ A ∧ ¬ x ∈ A ↔ ¬ ∀ y x ∈ y ∧ y ∈ A → x ∈ A
17 3 13 16 3bitri ⊢ x E ∘ E ∖ E A ↔ ¬ ∀ y x ∈ y ∧ y ∈ A → x ∈ A
18 17 exbii ⊢ ∃ x x E ∘ E ∖ E A ↔ ∃ x ¬ ∀ y x ∈ y ∧ y ∈ A → x ∈ A
19 exnal ⊢ ∃ x ¬ ∀ y x ∈ y ∧ y ∈ A → x ∈ A ↔ ¬ ∀ x ∀ y x ∈ y ∧ y ∈ A → x ∈ A
20 2 18 19 3bitri ⊢ A ∈ ran ⁡ E ∘ E ∖ E ↔ ¬ ∀ x ∀ y x ∈ y ∧ y ∈ A → x ∈ A
21 20 con2bii ⊢ ∀ x ∀ y x ∈ y ∧ y ∈ A → x ∈ A ↔ ¬ A ∈ ran ⁡ E ∘ E ∖ E
22 dftr2 ⊢ Tr ⁡ A ↔ ∀ x ∀ y x ∈ y ∧ y ∈ A → x ∈ A
23 eldif ⊢ A ∈ V ∖ ran ⁡ E ∘ E ∖ E ↔ A ∈ V ∧ ¬ A ∈ ran ⁡ E ∘ E ∖ E
24 1 23 mpbiran ⊢ A ∈ V ∖ ran ⁡ E ∘ E ∖ E ↔ ¬ A ∈ ran ⁡ E ∘ E ∖ E
25 21 22 24 3bitr4i ⊢ Tr ⁡ A ↔ A ∈ V ∖ ran ⁡ E ∘ E ∖ E