Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pj1eu Structured version   Unicode version

Theorem pj1eu 16840
 Description: Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015.)
Hypotheses
Ref Expression
pj1eu.a
pj1eu.s
pj1eu.o
pj1eu.z Cntz
pj1eu.2 SubGrp
pj1eu.3 SubGrp
pj1eu.4
pj1eu.5
Assertion
Ref Expression
pj1eu
Distinct variable groups:   ,,   , ,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem pj1eu
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pj1eu.2 . . . 4 SubGrp
2 pj1eu.3 . . . 4 SubGrp
3 pj1eu.a . . . . 5
4 pj1eu.s . . . . 5
53, 4lsmelval 16795 . . . 4 SubGrp SubGrp
61, 2, 5syl2anc 661 . . 3
76biimpa 484 . 2
8 reeanv 3025 . . . . 5
9 eqtr2 2484 . . . . . . 7
10 pj1eu.o . . . . . . . . 9
11 pj1eu.z . . . . . . . . 9 Cntz
121ad2antrr 725 . . . . . . . . 9 SubGrp
132ad2antrr 725 . . . . . . . . 9 SubGrp
14 pj1eu.4 . . . . . . . . . 10
1514ad2antrr 725 . . . . . . . . 9
16 pj1eu.5 . . . . . . . . . 10
1716ad2antrr 725 . . . . . . . . 9
18 simplrl 761 . . . . . . . . 9
19 simplrr 762 . . . . . . . . 9
20 simprl 756 . . . . . . . . 9
21 simprr 757 . . . . . . . . 9
223, 10, 11, 12, 13, 15, 17, 18, 19, 20, 21subgdisjb 16837 . . . . . . . 8
23 simpl 457 . . . . . . . 8
2422, 23syl6bi 228 . . . . . . 7
259, 24syl5 32 . . . . . 6
2625rexlimdvva 2956 . . . . 5
278, 26syl5bir 218 . . . 4
2827ralrimivva 2878 . . 3