Theorem dmqsblocks

Description: If the pet span ( R |X. ( ' E | A ) ) partitions A , then every block u e. A is of the form [ v ] for some v that not only lies in the domain but also has at least one internal element c and at least one R -target b (cf. also the comments of qseq ). It makes explicit that pet gives active representatives for each block, without ever forcing v = u . (Contributed by Peter Mazsa, 23-Nov-2025)

	Ref	Expression
Assertion	dmqsblocks	⊢ ( ( dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) = 𝐴 → ∀ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∃ 𝑏 ∃ 𝑐 ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) )

Proof

Step	Hyp	Ref	Expression
1		qseq	⊢ ( ( dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) = 𝐴 ↔ ∀ 𝑢 ( 𝑢 ∈ 𝐴 ↔ ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) )
2		eqab2	⊢ ( ∀ 𝑢 ( 𝑢 ∈ 𝐴 ↔ ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) → ∀ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) )
3	1 2	sylbi	⊢ ( ( dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) = 𝐴 → ∀ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) )
4		rexanid	⊢ ( ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ( 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) ↔ ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) )
5		eldmxrncnvepres2	⊢ ( 𝑣 ∈ V → ( 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝑣 ∈ 𝐴 ∧ ∃ 𝑐 𝑐 ∈ 𝑣 ∧ ∃ 𝑏 𝑣 𝑅 𝑏 ) ) )
6	5	elv	⊢ ( 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝑣 ∈ 𝐴 ∧ ∃ 𝑐 𝑐 ∈ 𝑣 ∧ ∃ 𝑏 𝑣 𝑅 𝑏 ) )
7		3simpc	⊢ ( ( 𝑣 ∈ 𝐴 ∧ ∃ 𝑐 𝑐 ∈ 𝑣 ∧ ∃ 𝑏 𝑣 𝑅 𝑏 ) → ( ∃ 𝑐 𝑐 ∈ 𝑣 ∧ ∃ 𝑏 𝑣 𝑅 𝑏 ) )
8	6 7	sylbi	⊢ ( 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) → ( ∃ 𝑐 𝑐 ∈ 𝑣 ∧ ∃ 𝑏 𝑣 𝑅 𝑏 ) )
9		exdistrv	⊢ ( ∃ 𝑐 ∃ 𝑏 ( 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) ↔ ( ∃ 𝑐 𝑐 ∈ 𝑣 ∧ ∃ 𝑏 𝑣 𝑅 𝑏 ) )
10		excom	⊢ ( ∃ 𝑐 ∃ 𝑏 ( 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) ↔ ∃ 𝑏 ∃ 𝑐 ( 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) )
11	9 10	bitr3i	⊢ ( ( ∃ 𝑐 𝑐 ∈ 𝑣 ∧ ∃ 𝑏 𝑣 𝑅 𝑏 ) ↔ ∃ 𝑏 ∃ 𝑐 ( 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) )
12	8 11	sylib	⊢ ( 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) → ∃ 𝑏 ∃ 𝑐 ( 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) )
13	12	anim1ci	⊢ ( ( 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) → ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ ∃ 𝑏 ∃ 𝑐 ( 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) ) )
14		3anass	⊢ ( ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) ↔ ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ ( 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) ) )
15	14	2exbii	⊢ ( ∃ 𝑏 ∃ 𝑐 ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) ↔ ∃ 𝑏 ∃ 𝑐 ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ ( 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) ) )
16		19.42vv	⊢ ( ∃ 𝑏 ∃ 𝑐 ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ ( 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) ) ↔ ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ ∃ 𝑏 ∃ 𝑐 ( 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) ) )
17	15 16	sylbbr	⊢ ( ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ ∃ 𝑏 ∃ 𝑐 ( 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) ) → ∃ 𝑏 ∃ 𝑐 ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) )
18	13 17	syl	⊢ ( ( 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) → ∃ 𝑏 ∃ 𝑐 ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) )
19	18	reximi	⊢ ( ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ( 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) → ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∃ 𝑏 ∃ 𝑐 ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) )
20	4 19	sylbir	⊢ ( ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) → ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∃ 𝑏 ∃ 𝑐 ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) )
21	20	ralimi	⊢ ( ∀ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) → ∀ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∃ 𝑏 ∃ 𝑐 ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) )
22	3 21	syl	⊢ ( ( dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) = 𝐴 → ∀ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∃ 𝑏 ∃ 𝑐 ( 𝑢 = [ 𝑣 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) )