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

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 ) ) )