Metamath Proof Explorer


Theorem erovlem

Description: Lemma for erov and eroprf . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 30-Dec-2014)

Ref Expression
Hypotheses eropr.1 J = A / R
eropr.2 K = B / S
eropr.3 φ T Z
eropr.4 φ R Er U
eropr.5 φ S Er V
eropr.6 φ T Er W
eropr.7 φ A U
eropr.8 φ B V
eropr.9 φ C W
eropr.10 φ + ˙ : A × B C
eropr.11 φ r A s A t B u B r R s t S u r + ˙ t T s + ˙ u
eropr.12 ˙ = x y z | p A q B x = p R y = q S z = p + ˙ q T
Assertion erovlem φ ˙ = x J , y K ι z | p A q B x = p R y = q S z = p + ˙ q T

Proof

Step Hyp Ref Expression
1 eropr.1 J = A / R
2 eropr.2 K = B / S
3 eropr.3 φ T Z
4 eropr.4 φ R Er U
5 eropr.5 φ S Er V
6 eropr.6 φ T Er W
7 eropr.7 φ A U
8 eropr.8 φ B V
9 eropr.9 φ C W
10 eropr.10 φ + ˙ : A × B C
11 eropr.11 φ r A s A t B u B r R s t S u r + ˙ t T s + ˙ u
12 eropr.12 ˙ = x y z | p A q B x = p R y = q S z = p + ˙ q T
13 simpl x = p R y = q S z = p + ˙ q T x = p R y = q S
14 13 reximi q B x = p R y = q S z = p + ˙ q T q B x = p R y = q S
15 14 reximi p A q B x = p R y = q S z = p + ˙ q T p A q B x = p R y = q S
16 1 eleq2i x J x A / R
17 vex x V
18 17 elqs x A / R p A x = p R
19 16 18 bitri x J p A x = p R
20 2 eleq2i y K y B / S
21 vex y V
22 21 elqs y B / S q B y = q S
23 20 22 bitri y K q B y = q S
24 19 23 anbi12i x J y K p A x = p R q B y = q S
25 reeanv p A q B x = p R y = q S p A x = p R q B y = q S
26 24 25 bitr4i x J y K p A q B x = p R y = q S
27 15 26 sylibr p A q B x = p R y = q S z = p + ˙ q T x J y K
28 27 pm4.71ri p A q B x = p R y = q S z = p + ˙ q T x J y K p A q B x = p R y = q S z = p + ˙ q T
29 1 2 3 4 5 6 7 8 9 10 11 eroveu φ x J y K ∃! z p A q B x = p R y = q S z = p + ˙ q T
30 iota1 ∃! z p A q B x = p R y = q S z = p + ˙ q T p A q B x = p R y = q S z = p + ˙ q T ι z | p A q B x = p R y = q S z = p + ˙ q T = z
31 29 30 syl φ x J y K p A q B x = p R y = q S z = p + ˙ q T ι z | p A q B x = p R y = q S z = p + ˙ q T = z
32 eqcom ι z | p A q B x = p R y = q S z = p + ˙ q T = z z = ι z | p A q B x = p R y = q S z = p + ˙ q T
33 31 32 bitrdi φ x J y K p A q B x = p R y = q S z = p + ˙ q T z = ι z | p A q B x = p R y = q S z = p + ˙ q T
34 33 pm5.32da φ x J y K p A q B x = p R y = q S z = p + ˙ q T x J y K z = ι z | p A q B x = p R y = q S z = p + ˙ q T
35 28 34 syl5bb φ p A q B x = p R y = q S z = p + ˙ q T x J y K z = ι z | p A q B x = p R y = q S z = p + ˙ q T
36 35 oprabbidv φ x y z | p A q B x = p R y = q S z = p + ˙ q T = x y z | x J y K z = ι z | p A q B x = p R y = q S z = p + ˙ q T
37 df-mpo x J , y K ι z | p A q B x = p R y = q S z = p + ˙ q T = x y w | x J y K w = ι z | p A q B x = p R y = q S z = p + ˙ q T
38 nfv w x J y K z = ι z | p A q B x = p R y = q S z = p + ˙ q T
39 nfv z x J y K
40 nfiota1 _ z ι z | p A q B x = p R y = q S z = p + ˙ q T
41 40 nfeq2 z w = ι z | p A q B x = p R y = q S z = p + ˙ q T
42 39 41 nfan z x J y K w = ι z | p A q B x = p R y = q S z = p + ˙ q T
43 eqeq1 z = w z = ι z | p A q B x = p R y = q S z = p + ˙ q T w = ι z | p A q B x = p R y = q S z = p + ˙ q T
44 43 anbi2d z = w x J y K z = ι z | p A q B x = p R y = q S z = p + ˙ q T x J y K w = ι z | p A q B x = p R y = q S z = p + ˙ q T
45 38 42 44 cbvoprab3 x y z | x J y K z = ι z | p A q B x = p R y = q S z = p + ˙ q T = x y w | x J y K w = ι z | p A q B x = p R y = q S z = p + ˙ q T
46 37 45 eqtr4i x J , y K ι z | p A q B x = p R y = q S z = p + ˙ q T = x y z | x J y K z = ι z | p A q B x = p R y = q S z = p + ˙ q T
47 36 12 46 3eqtr4g φ ˙ = x J , y K ι z | p A q B x = p R y = q S z = p + ˙ q T