Metamath Proof Explorer

Theorem cotr2g

Description: Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 for the main application. (Contributed by RP, 22-Mar-2020)

Ref Expression
Hypotheses cotr2g.d 
|- dom B C_ D
cotr2g.e 
|- ( ran B i^i dom A ) C_ E
cotr2g.f 
|- ran A C_ F
Assertion cotr2g 
|- ( ( A o. B ) C_ C <-> A. x e. D A. y e. E A. z e. F ( ( x B y /\ y A z ) -> x C z ) )

Proof

Step Hyp Ref Expression
1 cotr2g.d 
 |-  dom B C_ D
2 cotr2g.e 
 |-  ( ran B i^i dom A ) C_ E
3 cotr2g.f 
 |-  ran A C_ F
4 cotrg 
 |-  ( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) )
5 nfv 
 |-  F/ y x e. D
6 nfv 
 |-  F/ z x e. D
7 5 6 19.21-2 
 |-  ( A. y A. z ( x e. D -> ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) ) <-> ( x e. D -> A. y A. z ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) ) )
8 7 albii 
 |-  ( A. x A. y A. z ( x e. D -> ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) ) <-> A. x ( x e. D -> A. y A. z ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) ) )
9 simpl 
 |-  ( ( x B y /\ y A z ) -> x B y )
10 id 
 |-  ( ( x B y /\ y A z ) -> ( x B y /\ y A z ) )
11 simpr 
 |-  ( ( x B y /\ y A z ) -> y A z )
12 9 10 11 3jca 
 |-  ( ( x B y /\ y A z ) -> ( x B y /\ ( x B y /\ y A z ) /\ y A z ) )
13 simp2 
 |-  ( ( x B y /\ ( x B y /\ y A z ) /\ y A z ) -> ( x B y /\ y A z ) )
14 12 13 impbii 
 |-  ( ( x B y /\ y A z ) <-> ( x B y /\ ( x B y /\ y A z ) /\ y A z ) )
15 vex 
 |-  x e. _V
16 vex 
 |-  y e. _V
17 15 16 breldm 
 |-  ( x B y -> x e. dom B )
18 1 17 sseldi 
 |-  ( x B y -> x e. D )
19 18 pm4.71ri 
 |-  ( x B y <-> ( x e. D /\ x B y ) )
20 15 16 brelrn 
 |-  ( x B y -> y e. ran B )
21 vex 
 |-  z e. _V
22 16 21 breldm 
 |-  ( y A z -> y e. dom A )
23 elin 
 |-  ( y e. ( ran B i^i dom A ) <-> ( y e. ran B /\ y e. dom A ) )
24 23 biimpri 
 |-  ( ( y e. ran B /\ y e. dom A ) -> y e. ( ran B i^i dom A ) )
25 20 22 24 syl2an 
 |-  ( ( x B y /\ y A z ) -> y e. ( ran B i^i dom A ) )
26 2 25 sseldi 
 |-  ( ( x B y /\ y A z ) -> y e. E )
27 26 pm4.71ri 
 |-  ( ( x B y /\ y A z ) <-> ( y e. E /\ ( x B y /\ y A z ) ) )
28 16 21 brelrn 
 |-  ( y A z -> z e. ran A )
29 3 28 sseldi 
 |-  ( y A z -> z e. F )
30 29 pm4.71ri 
 |-  ( y A z <-> ( z e. F /\ y A z ) )
31 19 27 30 3anbi123i 
 |-  ( ( x B y /\ ( x B y /\ y A z ) /\ y A z ) <-> ( ( x e. D /\ x B y ) /\ ( y e. E /\ ( x B y /\ y A z ) ) /\ ( z e. F /\ y A z ) ) )
32 3an6 
 |-  ( ( ( x e. D /\ x B y ) /\ ( y e. E /\ ( x B y /\ y A z ) ) /\ ( z e. F /\ y A z ) ) <-> ( ( x e. D /\ y e. E /\ z e. F ) /\ ( x B y /\ ( x B y /\ y A z ) /\ y A z ) ) )
33 13 12 impbii 
 |-  ( ( x B y /\ ( x B y /\ y A z ) /\ y A z ) <-> ( x B y /\ y A z ) )
34 33 anbi2i 
 |-  ( ( ( x e. D /\ y e. E /\ z e. F ) /\ ( x B y /\ ( x B y /\ y A z ) /\ y A z ) ) <-> ( ( x e. D /\ y e. E /\ z e. F ) /\ ( x B y /\ y A z ) ) )
35 32 34 bitri 
 |-  ( ( ( x e. D /\ x B y ) /\ ( y e. E /\ ( x B y /\ y A z ) ) /\ ( z e. F /\ y A z ) ) <-> ( ( x e. D /\ y e. E /\ z e. F ) /\ ( x B y /\ y A z ) ) )
36 14 31 35 3bitri 
 |-  ( ( x B y /\ y A z ) <-> ( ( x e. D /\ y e. E /\ z e. F ) /\ ( x B y /\ y A z ) ) )
37 36 imbi1i 
 |-  ( ( ( x B y /\ y A z ) -> x C z ) <-> ( ( ( x e. D /\ y e. E /\ z e. F ) /\ ( x B y /\ y A z ) ) -> x C z ) )
38 impexp 
 |-  ( ( ( ( x e. D /\ y e. E /\ z e. F ) /\ ( x B y /\ y A z ) ) -> x C z ) <-> ( ( x e. D /\ y e. E /\ z e. F ) -> ( ( x B y /\ y A z ) -> x C z ) ) )
39 3impexp 
 |-  ( ( ( x e. D /\ y e. E /\ z e. F ) -> ( ( x B y /\ y A z ) -> x C z ) ) <-> ( x e. D -> ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) ) )
40 37 38 39 3bitri 
 |-  ( ( ( x B y /\ y A z ) -> x C z ) <-> ( x e. D -> ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) ) )
41 40 albii 
 |-  ( A. z ( ( x B y /\ y A z ) -> x C z ) <-> A. z ( x e. D -> ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) ) )
42 41 2albii 
 |-  ( A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) <-> A. x A. y A. z ( x e. D -> ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) ) )
43 df-ral 
 |-  ( A. x e. D A. y A. z ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) <-> A. x ( x e. D -> A. y A. z ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) ) )
44 8 42 43 3bitr4i 
 |-  ( A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) <-> A. x e. D A. y A. z ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) )
45 df-ral 
 |-  ( A. y e. E A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) <-> A. y ( y e. E -> A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) )
46 19.21v 
 |-  ( A. z ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) <-> ( y e. E -> A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) )
47 46 bicomi 
 |-  ( ( y e. E -> A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) <-> A. z ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) )
48 47 albii 
 |-  ( A. y ( y e. E -> A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) <-> A. y A. z ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) )
49 45 48 bitri 
 |-  ( A. y e. E A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) <-> A. y A. z ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) )
50 49 bicomi 
 |-  ( A. y A. z ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) <-> A. y e. E A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) )
51 50 ralbii 
 |-  ( A. x e. D A. y A. z ( y e. E -> ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) ) <-> A. x e. D A. y e. E A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) )
52 44 51 bitri 
 |-  ( A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) <-> A. x e. D A. y e. E A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) )
53 df-ral 
 |-  ( A. z e. F ( ( x B y /\ y A z ) -> x C z ) <-> A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) )
54 53 bicomi 
 |-  ( A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) <-> A. z e. F ( ( x B y /\ y A z ) -> x C z ) )
55 54 ralbii 
 |-  ( A. y e. E A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) <-> A. y e. E A. z e. F ( ( x B y /\ y A z ) -> x C z ) )
56 55 ralbii 
 |-  ( A. x e. D A. y e. E A. z ( z e. F -> ( ( x B y /\ y A z ) -> x C z ) ) <-> A. x e. D A. y e. E A. z e. F ( ( x B y /\ y A z ) -> x C z ) )
57 4 52 56 3bitri 
 |-  ( ( A o. B ) C_ C <-> A. x e. D A. y e. E A. z e. F ( ( x B y /\ y A z ) -> x C z ) )