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 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ∀ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) 𝑢 = 𝑣 )