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 |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) = A -> A. u e. A E. v e. dom ( R |X. ( `' _E |` A ) ) E. b E. c ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ c e. v /\ v R b ) )

Proof

Step Hyp Ref Expression
1 qseq 
 |-  ( ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) = A <-> A. u ( u e. A <-> E. v e. dom ( R |X. ( `' _E |` A ) ) u = [ v ] ( R |X. ( `' _E |` A ) ) ) )
2 eqab2 
 |-  ( A. u ( u e. A <-> E. v e. dom ( R |X. ( `' _E |` A ) ) u = [ v ] ( R |X. ( `' _E |` A ) ) ) -> A. u e. A E. v e. dom ( R |X. ( `' _E |` A ) ) u = [ v ] ( R |X. ( `' _E |` A ) ) )
3 1 2 sylbi 
 |-  ( ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) = A -> A. u e. A E. v e. dom ( R |X. ( `' _E |` A ) ) u = [ v ] ( R |X. ( `' _E |` A ) ) )
4 rexanid 
 |-  ( E. v e. dom ( R |X. ( `' _E |` A ) ) ( v e. dom ( R |X. ( `' _E |` A ) ) /\ u = [ v ] ( R |X. ( `' _E |` A ) ) ) <-> E. v e. dom ( R |X. ( `' _E |` A ) ) u = [ v ] ( R |X. ( `' _E |` A ) ) )
5 eldmxrncnvepres2 
 |-  ( v e. _V -> ( v e. dom ( R |X. ( `' _E |` A ) ) <-> ( v e. A /\ E. c c e. v /\ E. b v R b ) ) )
6 5 elv 
 |-  ( v e. dom ( R |X. ( `' _E |` A ) ) <-> ( v e. A /\ E. c c e. v /\ E. b v R b ) )
7 3simpc 
 |-  ( ( v e. A /\ E. c c e. v /\ E. b v R b ) -> ( E. c c e. v /\ E. b v R b ) )
8 6 7 sylbi 
 |-  ( v e. dom ( R |X. ( `' _E |` A ) ) -> ( E. c c e. v /\ E. b v R b ) )
9 exdistrv 
 |-  ( E. c E. b ( c e. v /\ v R b ) <-> ( E. c c e. v /\ E. b v R b ) )
10 excom 
 |-  ( E. c E. b ( c e. v /\ v R b ) <-> E. b E. c ( c e. v /\ v R b ) )
11 9 10 bitr3i 
 |-  ( ( E. c c e. v /\ E. b v R b ) <-> E. b E. c ( c e. v /\ v R b ) )
12 8 11 sylib 
 |-  ( v e. dom ( R |X. ( `' _E |` A ) ) -> E. b E. c ( c e. v /\ v R b ) )
13 12 anim1ci 
 |-  ( ( v e. dom ( R |X. ( `' _E |` A ) ) /\ u = [ v ] ( R |X. ( `' _E |` A ) ) ) -> ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ E. b E. c ( c e. v /\ v R b ) ) )
14 3anass 
 |-  ( ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ c e. v /\ v R b ) <-> ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ ( c e. v /\ v R b ) ) )
15 14 2exbii 
 |-  ( E. b E. c ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ c e. v /\ v R b ) <-> E. b E. c ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ ( c e. v /\ v R b ) ) )
16 19.42vv 
 |-  ( E. b E. c ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ ( c e. v /\ v R b ) ) <-> ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ E. b E. c ( c e. v /\ v R b ) ) )
17 15 16 sylbbr 
 |-  ( ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ E. b E. c ( c e. v /\ v R b ) ) -> E. b E. c ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ c e. v /\ v R b ) )
18 13 17 syl 
 |-  ( ( v e. dom ( R |X. ( `' _E |` A ) ) /\ u = [ v ] ( R |X. ( `' _E |` A ) ) ) -> E. b E. c ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ c e. v /\ v R b ) )
19 18 reximi 
 |-  ( E. v e. dom ( R |X. ( `' _E |` A ) ) ( v e. dom ( R |X. ( `' _E |` A ) ) /\ u = [ v ] ( R |X. ( `' _E |` A ) ) ) -> E. v e. dom ( R |X. ( `' _E |` A ) ) E. b E. c ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ c e. v /\ v R b ) )
20 4 19 sylbir 
 |-  ( E. v e. dom ( R |X. ( `' _E |` A ) ) u = [ v ] ( R |X. ( `' _E |` A ) ) -> E. v e. dom ( R |X. ( `' _E |` A ) ) E. b E. c ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ c e. v /\ v R b ) )
21 20 ralimi 
 |-  ( A. u e. A E. v e. dom ( R |X. ( `' _E |` A ) ) u = [ v ] ( R |X. ( `' _E |` A ) ) -> A. u e. A E. v e. dom ( R |X. ( `' _E |` A ) ) E. b E. c ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ c e. v /\ v R b ) )
22 3 21 syl 
 |-  ( ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) = A -> A. u e. A E. v e. dom ( R |X. ( `' _E |` A ) ) E. b E. c ( u = [ v ] ( R |X. ( `' _E |` A ) ) /\ c e. v /\ v R b ) )