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

Metamath Proof Explorer

Theorem dfeldisj3

Description: Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021)

Ref Expression
Assertion dfeldisj3 ( ElDisj 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ∀ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) 𝑢 = 𝑣 )

Proof

Step Hyp Ref Expression
1 df-eldisj ⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) )
2 relres ⊢ Rel ( ◡ E ↾ 𝐴 )
3 dfdisjALTV3 ⊢ ( Disj ( ◡ E ↾ 𝐴 ) ↔ ( ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ∧ 𝑣 ( ◡ E ↾ 𝐴 ) 𝑥 ) → 𝑢 = 𝑣 ) ∧ Rel ( ◡ E ↾ 𝐴 ) ) )
4 2 3 mpbiran2 ⊢ ( Disj ( ◡ E ↾ 𝐴 ) ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ∧ 𝑣 ( ◡ E ↾ 𝐴 ) 𝑥 ) → 𝑢 = 𝑣 ) )
5 an4 ⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ 𝑣 ) ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣 ) ) )
6 brcnvepres ⊢ ( ( 𝑢 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) )
7 6 el2v ⊢ ( 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) )
8 brcnvepres ⊢ ( ( 𝑣 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑣 ( ◡ E ↾ 𝐴 ) 𝑥 ↔ ( 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ 𝑣 ) ) )
9 8 el2v ⊢ ( 𝑣 ( ◡ E ↾ 𝐴 ) 𝑥 ↔ ( 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ 𝑣 ) )
10 7 9 anbi12i ⊢ ( ( 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ∧ 𝑣 ( ◡ E ↾ 𝐴 ) 𝑥 ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ 𝑣 ) ) )
11 elin ⊢ ( 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ↔ ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣 ) )
12 11 anbi2i ⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣 ) ) )
13 5 10 12 3bitr4i ⊢ ( ( 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ∧ 𝑣 ( ◡ E ↾ 𝐴 ) 𝑥 ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) )
14 df-3an ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) )
15 13 14 bitr4i ⊢ ( ( 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ∧ 𝑣 ( ◡ E ↾ 𝐴 ) 𝑥 ) ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) )
16 15 imbi1i ⊢ ( ( ( 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ∧ 𝑣 ( ◡ E ↾ 𝐴 ) 𝑥 ) → 𝑢 = 𝑣 ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) → 𝑢 = 𝑣 ) )
17 16 3albii ⊢ ( ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ∧ 𝑣 ( ◡ E ↾ 𝐴 ) 𝑥 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) → 𝑢 = 𝑣 ) )
18 1 4 17 3bitri ⊢ ( ElDisj 𝐴 ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) → 𝑢 = 𝑣 ) )
19 r3al ⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ∀ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) 𝑢 = 𝑣 ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) → 𝑢 = 𝑣 ) )
20 18 19 bitr4i ⊢ ( ElDisj 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ∀ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) 𝑢 = 𝑣 )