Theorem dfeldisj5

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

	Ref	Expression
Assertion	dfeldisj5	⊢ ( ElDisj 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		dfeldisj4	⊢ ( ElDisj 𝐴 ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )
2		inecmo2	⊢ ( ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ∧ Rel ◡ E ) ↔ ( ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 ∧ Rel ◡ E ) )
3		relcnv	⊢ Rel ◡ E
4	3	biantru	⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ↔ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ∧ Rel ◡ E ) )
5	3	biantru	⊢ ( ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 ↔ ( ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 ∧ Rel ◡ E ) )
6	2 4 5	3bitr4i	⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 )
7		eccnvep	⊢ ( 𝑢 ∈ V → [ 𝑢 ] ◡ E = 𝑢 )
8	7	elv	⊢ [ 𝑢 ] ◡ E = 𝑢
9		eccnvep	⊢ ( 𝑣 ∈ V → [ 𝑣 ] ◡ E = 𝑣 )
10	9	elv	⊢ [ 𝑣 ] ◡ E = 𝑣
11	8 10	ineq12i	⊢ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ( 𝑢 ∩ 𝑣 )
12	11	eqeq1i	⊢ ( ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ↔ ( 𝑢 ∩ 𝑣 ) = ∅ )
13	12	orbi2i	⊢ ( ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ↔ ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
14	13	2ralbii	⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
15		brcnvep	⊢ ( 𝑢 ∈ V → ( 𝑢 ◡ E 𝑥 ↔ 𝑥 ∈ 𝑢 ) )
16	15	elv	⊢ ( 𝑢 ◡ E 𝑥 ↔ 𝑥 ∈ 𝑢 )
17	16	rmobii	⊢ ( ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 ↔ ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )
18	17	albii	⊢ ( ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )
19	6 14 18	3bitr3i	⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )
20	1 19	bitr4i	⊢ ( ElDisj 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) )