Theorem disjsuc

Description: Disjoint range Cartesian product, special case. (Contributed by Peter Mazsa, 25-Aug-2023)

	Ref	Expression
Assertion	disjsuc	⊢ ( 𝐴 ∈ 𝑉 → ( Disj ( 𝑅 ⋉ ( ◡ E ↾ suc 𝐴 ) ) ↔ ( Disj ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ ∀ 𝑢 ∈ 𝐴 ( ( 𝑢 ∩ 𝐴 ) = ∅ ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		disjsuc2	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ ( 𝐴 ∪ { 𝐴 } ) ∀ 𝑣 ∈ ( 𝐴 ∪ { 𝐴 } ) ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ◡ E ) ) = ∅ ) ↔ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ◡ E ) ) = ∅ ) ∧ ∀ 𝑢 ∈ 𝐴 ( ( 𝑢 ∩ 𝐴 ) = ∅ ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) ) )
2		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
3	2	reseq2i	⊢ ( ◡ E ↾ suc 𝐴 ) = ( ◡ E ↾ ( 𝐴 ∪ { 𝐴 } ) )
4	3	xrneq2i	⊢ ( 𝑅 ⋉ ( ◡ E ↾ suc 𝐴 ) ) = ( 𝑅 ⋉ ( ◡ E ↾ ( 𝐴 ∪ { 𝐴 } ) ) )
5	4	disjeqi	⊢ ( Disj ( 𝑅 ⋉ ( ◡ E ↾ suc 𝐴 ) ) ↔ Disj ( 𝑅 ⋉ ( ◡ E ↾ ( 𝐴 ∪ { 𝐴 } ) ) ) )
6		disjxrnres5	⊢ ( Disj ( 𝑅 ⋉ ( ◡ E ↾ ( 𝐴 ∪ { 𝐴 } ) ) ) ↔ ∀ 𝑢 ∈ ( 𝐴 ∪ { 𝐴 } ) ∀ 𝑣 ∈ ( 𝐴 ∪ { 𝐴 } ) ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ◡ E ) ) = ∅ ) )
7	5 6	bitri	⊢ ( Disj ( 𝑅 ⋉ ( ◡ E ↾ suc 𝐴 ) ) ↔ ∀ 𝑢 ∈ ( 𝐴 ∪ { 𝐴 } ) ∀ 𝑣 ∈ ( 𝐴 ∪ { 𝐴 } ) ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ◡ E ) ) = ∅ ) )
8		disjxrnres5	⊢ ( Disj ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ◡ E ) ) = ∅ ) )
9	8	anbi1i	⊢ ( ( Disj ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ ∀ 𝑢 ∈ 𝐴 ( ( 𝑢 ∩ 𝐴 ) = ∅ ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) ↔ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ ◡ E ) ∩ [ 𝑣 ] ( 𝑅 ⋉ ◡ E ) ) = ∅ ) ∧ ∀ 𝑢 ∈ 𝐴 ( ( 𝑢 ∩ 𝐴 ) = ∅ ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) )
10	1 7 9	3bitr4g	⊢ ( 𝐴 ∈ 𝑉 → ( Disj ( 𝑅 ⋉ ( ◡ E ↾ suc 𝐴 ) ) ↔ ( Disj ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ ∀ 𝑢 ∈ 𝐴 ( ( 𝑢 ∩ 𝐴 ) = ∅ ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) ) )