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 𝐴 ∈ V
Assertion dftr6 ( Tr 𝐴𝐴 ∈ ( V ∖ ran ( ( E ∘ E ) ∖ E ) ) )

Proof

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