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

Metamath Proof Explorer

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 ↾ 𝐴 ) ) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣 𝑅 𝑏 ) )