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 ⁡ R ⋉ E -1 ↾ A / R ⋉ E -1 ↾ A = A → ∀ u ∈ A ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A ∃ b ∃ c u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b

Proof

Step Hyp Ref Expression
1 qseq ⊢ dom ⁡ R ⋉ E -1 ↾ A / R ⋉ E -1 ↾ A = A ↔ ∀ u u ∈ A ↔ ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A u = v R ⋉ E -1 ↾ A
2 eqab2 ⊢ ∀ u u ∈ A ↔ ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A u = v R ⋉ E -1 ↾ A → ∀ u ∈ A ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A u = v R ⋉ E -1 ↾ A
3 1 2 sylbi ⊢ dom ⁡ R ⋉ E -1 ↾ A / R ⋉ E -1 ↾ A = A → ∀ u ∈ A ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A u = v R ⋉ E -1 ↾ A
4 rexanid ⊢ ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A v ∈ dom ⁡ R ⋉ E -1 ↾ A ∧ u = v R ⋉ E -1 ↾ A ↔ ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A u = v R ⋉ E -1 ↾ A
5 eldmxrncnvepres2 ⊢ v ∈ V → v ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ v ∈ A ∧ ∃ c c ∈ v ∧ ∃ b v R b
6 5 elv ⊢ v ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ v ∈ A ∧ ∃ c c ∈ v ∧ ∃ b v R b
7 3simpc ⊢ v ∈ A ∧ ∃ c c ∈ v ∧ ∃ b v R b → ∃ c c ∈ v ∧ ∃ b v R b
8 6 7 sylbi ⊢ v ∈ dom ⁡ R ⋉ E -1 ↾ A → ∃ c c ∈ v ∧ ∃ b v R b
9 exdistrv ⊢ ∃ c ∃ b c ∈ v ∧ v R b ↔ ∃ c c ∈ v ∧ ∃ b v R b
10 excom ⊢ ∃ c ∃ b c ∈ v ∧ v R b ↔ ∃ b ∃ c c ∈ v ∧ v R b
11 9 10 bitr3i ⊢ ∃ c c ∈ v ∧ ∃ b v R b ↔ ∃ b ∃ c c ∈ v ∧ v R b
12 8 11 sylib ⊢ v ∈ dom ⁡ R ⋉ E -1 ↾ A → ∃ b ∃ c c ∈ v ∧ v R b
13 12 anim1ci ⊢ v ∈ dom ⁡ R ⋉ E -1 ↾ A ∧ u = v R ⋉ E -1 ↾ A → u = v R ⋉ E -1 ↾ A ∧ ∃ b ∃ c c ∈ v ∧ v R b
14 3anass ⊢ u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b ↔ u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b
15 14 2exbii ⊢ ∃ b ∃ c u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b ↔ ∃ b ∃ c u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b
16 19.42vv ⊢ ∃ b ∃ c u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b ↔ u = v R ⋉ E -1 ↾ A ∧ ∃ b ∃ c c ∈ v ∧ v R b
17 15 16 sylbbr ⊢ u = v R ⋉ E -1 ↾ A ∧ ∃ b ∃ c c ∈ v ∧ v R b → ∃ b ∃ c u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b
18 13 17 syl ⊢ v ∈ dom ⁡ R ⋉ E -1 ↾ A ∧ u = v R ⋉ E -1 ↾ A → ∃ b ∃ c u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b
19 18 reximi ⊢ ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A v ∈ dom ⁡ R ⋉ E -1 ↾ A ∧ u = v R ⋉ E -1 ↾ A → ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A ∃ b ∃ c u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b
20 4 19 sylbir ⊢ ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A u = v R ⋉ E -1 ↾ A → ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A ∃ b ∃ c u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b
21 20 ralimi ⊢ ∀ u ∈ A ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A u = v R ⋉ E -1 ↾ A → ∀ u ∈ A ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A ∃ b ∃ c u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b
22 3 21 syl ⊢ dom ⁡ R ⋉ E -1 ↾ A / R ⋉ E -1 ↾ A = A → ∀ u ∈ A ∃ v ∈ dom ⁡ R ⋉ E -1 ↾ A ∃ b ∃ c u = v R ⋉ E -1 ↾ A ∧ c ∈ v ∧ v R b