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

Theorem fpwwe2lem8 8512
 Description: Lemma for fpwwe2 8518. Show by induction that the two isometries and agree on their common domain. (Contributed by Mario Carneiro, 15-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1
fpwwe2.2
fpwwe2.3
fpwwe2lem9.x
fpwwe2lem9.y
fpwwe2lem9.m OrdIso
fpwwe2lem9.n OrdIso
fpwwe2lem9.s
Assertion
Ref Expression
fpwwe2lem8
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,   ,,,,   ,,,,   ,,,,   ,,,,
Allowed substitution hints:   (,)

Proof of Theorem fpwwe2lem8
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fpwwe2lem9.m . . . 4 OrdIso
21oif 7499 . . 3
3 ffn 5591 . . 3
42, 3mp1i 12 . 2
5 fpwwe2lem9.n . . . . 5 OrdIso
65oif 7499 . . . 4
7 ffn 5591 . . . 4
86, 7mp1i 12 . . 3
9 fpwwe2lem9.s . . 3
10 fnssres 5558 . . 3
118, 9, 10syl2anc 643 . 2
121oicl 7498 . . . . . 6
13 ordelon 4605 . . . . . 6
1412, 13mpan 652 . . . . 5
15 eleq1 2496 . . . . . . . . 9
16 fveq2 5728 . . . . . . . . . 10
17 fveq2 5728 . . . . . . . . . 10
1816, 17eqeq12d 2450 . . . . . . . . 9
1915, 18imbi12d 312 . . . . . . . 8
2019imbi2d 308 . . . . . . 7
21 r19.21v 2793 . . . . . . . . 9
2212a1i 11 . . . . . . . . . . . . . . . . 17
23 ordelss 4597 . . . . . . . . . . . . . . . . 17
2422, 23sylan 458 . . . . . . . . . . . . . . . 16
2524sselda 3348 . . . . . . . . . . . . . . 15
26 pm2.27 37 . . . . . . . . . . . . . . 15
2725, 26syl 16 . . . . . . . . . . . . . 14
2827ralimdva 2784 . . . . . . . . . . . . 13
294adantr 452 . . . . . . . . . . . . . . . . 17
30 fnssres 5558 . . . . . . . . . . . . . . . . 17
3129, 24, 30syl2anc 643 . . . . . . . . . . . . . . . 16
328adantr 452 . . . . . . . . . . . . . . . . 17
339adantr 452 . . . . . . . . . . . . . . . . . 18
3424, 33sstrd 3358 . . . . . . . . . . . . . . . . 17
35 fnssres 5558 . . . . . . . . . . . . . . . . 17
3632, 34, 35syl2anc 643 . . . . . . . . . . . . . . . 16
37 eqfnfv 5827 . . . . . . . . . . . . . . . 16
3831, 36, 37syl2anc 643 . . . . . . . . . . . . . . 15
39 fvres 5745 . . . . . . . . . . . . . . . . 17
40 fvres 5745 . . . . . . . . . . . . . . . . 17
4139, 40eqeq12d 2450 . . . . . . . . . . . . . . . 16
4241ralbiia 2737 . . . . . . . . . . . . . . 15
4338, 42syl6bb 253 . . . . . . . . . . . . . 14
44 fpwwe2.1 . . . . . . . . . . . . . . . . . . . . . 22
45 fpwwe2.2 . . . . . . . . . . . . . . . . . . . . . . 23
4645ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
47 simpll 731 . . . . . . . . . . . . . . . . . . . . . . 23
48 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . 23
4947, 48sylan 458 . . . . . . . . . . . . . . . . . . . . . 22
50 fpwwe2lem9.x . . . . . . . . . . . . . . . . . . . . . . 23
5150ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
52 fpwwe2lem9.y . . . . . . . . . . . . . . . . . . . . . . 23
5352ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
54 simplr 732 . . . . . . . . . . . . . . . . . . . . . 22
559sselda 3348 . . . . . . . . . . . . . . . . . . . . . . 23
5655adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
57 simpr 448 . . . . . . . . . . . . . . . . . . . . . 22
5844, 46, 49, 51, 53, 1, 5, 54, 56, 57fpwwe2lem7 8511 . . . . . . . . . . . . . . . . . . . . 21
5958simpld 446 . . . . . . . . . . . . . . . . . . . 20
6057eqcomd 2441 . . . . . . . . . . . . . . . . . . . . . 22
6144, 46, 49, 53, 51, 5, 1, 56, 54, 60fpwwe2lem7 8511 . . . . . . . . . . . . . . . . . . . . 21
6261simpld 446 . . . . . . . . . . . . . . . . . . . 20
6359, 62impbida 806 . . . . . . . . . . . . . . . . . . 19
64 fvex 5742 . . . . . . . . . . . . . . . . . . . 20
65 vex 2959 . . . . . . . . . . . . . . . . . . . . 21
6665eliniseg 5233 . . . . . . . . . . . . . . . . . . . 20
6764, 66ax-mp 8 . . . . . . . . . . . . . . . . . . 19
68 fvex 5742 . . . . . . . . . . . . . . . . . . . 20
6965eliniseg 5233 . . . . . . . . . . . . . . . . . . . 20
7068, 69ax-mp 8 . . . . . . . . . . . . . . . . . . 19
7163, 67, 703bitr4g 280 . . . . . . . . . . . . . . . . . 18
7271eqrdv 2434 . . . . . . . . . . . . . . . . 17
73 inss2 3562 . . . . . . . . . . . . . . . . . . . 20
74 relxp 4983 . . . . . . . . . . . . . . . . . . . 20
75 relss 4963 . . . . . . . . . . . . . . . . . . . 20
7673, 74, 75mp2 9 . . . . . . . . . . . . . . . . . . 19
77 inss2 3562 . . . . . . . . . . . . . . . . . . . 20
78 relss 4963 . . . . . . . . . . . . . . . . . . . 20
7977, 74, 78mp2 9 . . . . . . . . . . . . . . . . . . 19
80 vex 2959 . . . . . . . . . . . . . . . . . . . . . . . . 25
8180eliniseg 5233 . . . . . . . . . . . . . . . . . . . . . . . 24
8266, 81anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . 23
8364, 82ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22
8458simprd 450 . . . . . . . . . . . . . . . . . . . . . . 23
8584impr 603 . . . . . . . . . . . . . . . . . . . . . 22
8683, 85sylan2b 462 . . . . . . . . . . . . . . . . . . . . 21
8786pm5.32da 623 . . . . . . . . . . . . . . . . . . . 20
88 brinxp2 4939 . . . . . . . . . . . . . . . . . . . . 21
89 df-br 4213 . . . . . . . . . . . . . . . . . . . . 21
90 df-3an 938 . . . . . . . . . . . . . . . . . . . . 21
9188, 89, 903bitr3i 267 . . . . . . . . . . . . . . . . . . . 20
92 brinxp2 4939 . . . . . . . . . . . . . . . . . . . . 21
93 df-br 4213 . . . . . . . . . . . . . . . . . . . . 21
94 df-3an 938 . . . . . . . . . . . . . . . . . . . . 21
9592, 93, 943bitr3i 267 . . . . . . . . . . . . . . . . . . . 20
9687, 91, 953bitr4g 280 . . . . . . . . . . . . . . . . . . 19
9776, 79, 96eqrelrdv 4972 . . . . . . . . . . . . . . . . . 18
9872, 72xpeq12d 4903 . . . . . . . . . . . . . . . . . . 19
9998ineq2d 3542 . . . . . . . . . . . . . . . . . 18
10097, 99eqtrd 2468 . . . . . . . . . . . . . . . . 17
10172, 100oveq12d 6099 . . . . . . . . . . . . . . . 16
1022ffvelrni 5869 . . . . . . . . . . . . . . . . . . 19
103102adantl 453 . . . . . . . . . . . . . . . . . 18
104103adantr 452 . . . . . . . . . . . . . . . . 17
10544, 45, 50fpwwe2lem3 8508 . . . . . . . . . . . . . . . . 17
10647, 104, 105syl2anc 643 . . . . . . . . . . . . . . . 16
1076ffvelrni 5869 . . . . . . . . . . . . . . . . . . 19
10855, 107syl 16 . . . . . . . . . . . . . . . . . 18
109108adantr 452 . . . . . . . . . . . . . . . . 17
11044, 45, 52fpwwe2lem3 8508 . . . . . . . . . . . . . . . . 17
11147, 109, 110syl2anc 643 . . . . . . . . . . . . . . . 16
112101, 106, 1113eqtr3d 2476 . . . . . . . . . . . . . . 15
113112ex 424 . . . . . . . . . . . . . 14
11443, 113sylbird 227 . . . . . . . . . . . . 13
11528, 114syld 42 . . . . . . . . . . . 12
116115ex 424 . . . . . . . . . . 11
117116com23 74 . . . . . . . . . 10
118117a2i 13 . . . . . . . . 9
11921, 118sylbi 188 . . . . . . . 8
120119a1i 11 . . . . . . 7
12120, 120tfis2 4836 . . . . . 6
122121com3l 77 . . . . 5
12314, 122mpdi 40 . . . 4
124123imp 419 . . 3
125 fvres 5745 . . . 4