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

Metamath Proof Explorer

Theorem disjsuc2

Description: Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023)

		Ref	Expression
	Assertion	disjsuc2	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ ( 𝐴 ∪ { 𝐴 } ) ∀ 𝑣 ∈ ( 𝐴 ∪ { 𝐴 } ) ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ) ↔ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ) ∧ ∀ 𝑢 ∈ 𝐴 ( ( 𝑢 ∩ 𝐴 ) = ∅ ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		disjressuc2	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ ( 𝐴 ∪ { 𝐴 } ) ∀ 𝑣 ∈ ( 𝐴 ∪ { 𝐴 } ) ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ) ↔ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ) ∧ ∀ 𝑢 ∈ 𝐴 ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝐴 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ) ) )
2		disjecxrncnvep	⊢ ( ( 𝑢 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝐴 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ↔ ( ( 𝑢 ∩ 𝐴 ) = ∅ ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) )
3	2	el2v1	⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝐴 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ↔ ( ( 𝑢 ∩ 𝐴 ) = ∅ ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) )
4	3	ralbidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ 𝐴 ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝐴 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ↔ ∀ 𝑢 ∈ 𝐴 ( ( 𝑢 ∩ 𝐴 ) = ∅ ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) )
5	4	anbi2d	⊢ ( 𝐴 ∈ 𝑉 → ( ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ) ∧ ∀ 𝑢 ∈ 𝐴 ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝐴 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ) ↔ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ) ∧ ∀ 𝑢 ∈ 𝐴 ( ( 𝑢 ∩ 𝐴 ) = ∅ ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) ) )
6	1 5	bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ ( 𝐴 ∪ { 𝐴 } ) ∀ 𝑣 ∈ ( 𝐴 ∪ { 𝐴 } ) ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ) ↔ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ^◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ^◡ E ) ) = ∅ ) ∧ ∀ 𝑢 ∈ 𝐴 ( ( 𝑢 ∩ 𝐴 ) = ∅ ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) ) )