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↔∃xxE∘E∖EA
3 brdif ⊢xE∘E∖EA↔xE∘EA∧¬xEA
4 vex ⊢x∈V
5 4 1 brco ⊢xE∘EA↔∃yxEy∧yEA
6 epel ⊢xEy↔x∈y
7 1 epeli ⊢yEA↔y∈A
8 6 7 anbi12i ⊢xEy∧yEA↔x∈y∧y∈A
9 8 exbii ⊢∃yxEy∧yEA↔∃yx∈y∧y∈A
10 5 9 bitri ⊢xE∘EA↔∃yx∈y∧y∈A
11 1 epeli ⊢xEA↔x∈A
12 11 notbii ⊢¬xEA↔¬x∈A
13 10 12 anbi12i ⊢xE∘EA∧¬xEA↔∃yx∈y∧y∈A∧¬x∈A
14 19.41v ⊢∃yx∈y∧y∈A∧¬x∈A↔∃yx∈y∧y∈A∧¬x∈A
15 exanali ⊢∃yx∈y∧y∈A∧¬x∈A↔¬∀yx∈y∧y∈A→x∈A
16 14 15 bitr3i ⊢∃yx∈y∧y∈A∧¬x∈A↔¬∀yx∈y∧y∈A→x∈A
17 3 13 16 3bitri ⊢xE∘E∖EA↔¬∀yx∈y∧y∈A→x∈A
18 17 exbii ⊢∃xxE∘E∖EA↔∃x¬∀yx∈y∧y∈A→x∈A
19 exnal ⊢∃x¬∀yx∈y∧y∈A→x∈A↔¬∀x∀yx∈y∧y∈A→x∈A
20 2 18 19 3bitri ⊢A∈ran⁡E∘E∖E↔¬∀x∀yx∈y∧y∈A→x∈A
21 20 con2bii ⊢∀x∀yx∈y∧y∈A→x∈A↔¬A∈ran⁡E∘E∖E
22 dftr2 ⊢Tr⁡A↔∀x∀yx∈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