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

Theorem fpwwe2lem13 9041
Description: Lemma for fpwwe2 9042. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1
fpwwe2.2
fpwwe2.3
fpwwe2.4
Assertion
Ref Expression
fpwwe2lem13
Distinct variable groups:   , , , ,   , , , ,   , , , ,   , ,   , , , ,

Proof of Theorem fpwwe2lem13
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssun2 3667 . . . 4
2 fpwwe2.1 . . . . . . . . . . . . . 14
3 fpwwe2.2 . . . . . . . . . . . . . . 15
43adantr 465 . . . . . . . . . . . . . 14
5 fpwwe2.3 . . . . . . . . . . . . . . 15
65adantlr 714 . . . . . . . . . . . . . 14
7 fpwwe2.4 . . . . . . . . . . . . . 14
82, 4, 6, 7fpwwe2lem12 9040 . . . . . . . . . . . . 13
92, 4, 6, 7fpwwe2lem11 9039 . . . . . . . . . . . . . 14
10 ffun 5738 . . . . . . . . . . . . . 14
11 funfvbrb 6000 . . . . . . . . . . . . . 14
129, 10, 113syl 20 . . . . . . . . . . . . 13
138, 12mpbid 210 . . . . . . . . . . . 12
142, 4fpwwe2lem2 9031 . . . . . . . . . . . 12
1513, 14mpbid 210 . . . . . . . . . . 11
1615simpld 459 . . . . . . . . . 10
1716simpld 459 . . . . . . . . 9
1816simprd 463 . . . . . . . . . . . 12
1915simprd 463 . . . . . . . . . . . . 13
2019simpld 459 . . . . . . . . . . . 12
2117, 18, 203jca 1176 . . . . . . . . . . 11
222, 3, 5fpwwe2lem5 9033 . . . . . . . . . . 11
2321, 22syldan 470 . . . . . . . . . 10
2423snssd 4175 . . . . . . . . 9
2517, 24unssd 3679 . . . . . . . 8
26 ssun1 3666 . . . . . . . . . . 11
27 xpss12 5113 . . . . . . . . . . 11
2826, 26, 27mp2an 672 . . . . . . . . . 10
2918, 28syl6ss 3515 . . . . . . . . 9
30 xpss12 5113 . . . . . . . . . . 11
3126, 1, 30mp2an 672 . . . . . . . . . 10
3231a1i 11 . . . . . . . . 9
3329, 32unssd 3679 . . . . . . . 8
3425, 33jca 532 . . . . . . 7
35 ssdif0 3885 . . . . . . . . . . . . . 14
36 simpllr 760 . . . . . . . . . . . . . . . . . 18
3718ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
3837ssbrd 4493 . . . . . . . . . . . . . . . . . . 19
39 brxp 5035 . . . . . . . . . . . . . . . . . . . 20
4039simplbi 460 . . . . . . . . . . . . . . . . . . 19
4138, 40syl6 33 . . . . . . . . . . . . . . . . . 18
4236, 41mtod 177 . . . . . . . . . . . . . . . . 17
43 brxp 5035 . . . . . . . . . . . . . . . . . . 19
4443simplbi 460 . . . . . . . . . . . . . . . . . 18
4536, 44nsyl 121 . . . . . . . . . . . . . . . . 17
46 ovex 6324 . . . . . . . . . . . . . . . . . . 19
47 breq2 4456 . . . . . . . . . . . . . . . . . . . . 21
48 brun 4500 . . . . . . . . . . . . . . . . . . . . 21
4947, 48syl6bb 261 . . . . . . . . . . . . . . . . . . . 20
5049notbid 294 . . . . . . . . . . . . . . . . . . 19
5146, 50rexsn 4069 . . . . . . . . . . . . . . . . . 18
52 ioran 490 . . . . . . . . . . . . . . . . . 18
5351, 52bitri 249 . . . . . . . . . . . . . . . . 17
5442, 45, 53sylanbrc 664 . . . . . . . . . . . . . . . 16
55 simplrr 762 . . . . . . . . . . . . . . . . . . 19
5655neneqd 2659 . . . . . . . . . . . . . . . . . 18
57 simpr 461 . . . . . . . . . . . . . . . . . . . 20
58 sssn 4188 . . . . . . . . . . . . . . . . . . . 20
5957, 58sylib 196 . . . . . . . . . . . . . . . . . . 19
6059ord 377 . . . . . . . . . . . . . . . . . 18
6156, 60mpd 15 . . . . . . . . . . . . . . . . 17
6261raleqdv 3060 . . . . . . . . . . . . . . . . . 18
63 breq1 4455 . . . . . . . . . . . . . . . . . . . 20
6463notbid 294 . . . . . . . . . . . . . . . . . . 19
6546, 64ralsn 4068 . . . . . . . . . . . . . . . . . 18
6662, 65syl6bb 261 . . . . . . . . . . . . . . . . 17
6761, 66rexeqbidv 3069 . . . . . . . . . . . . . . . 16
6854, 67mpbird 232 . . . . . . . . . . . . . . 15
6968ex 434 . . . . . . . . . . . . . 14
7035, 69syl5bir 218 . . . . . . . . . . . . 13
71 vex 3112 . . . . . . . . . . . . . . . . 17
72 difexg 4600 . . . . . . . . . . . . . . . . 17
7371, 72mp1i 12 . . . . . . . . . . . . . . . 16
74 wefr 4874 . . . . . . . . . . . . . . . . . 18
7520, 74syl 16 . . . . . . . . . . . . . . . . 17
7675ad2antrr 725 . . . . . . . . . . . . . . . 16
77 simplrl 761 . . . . . . . . . . . . . . . . . 18
78 uncom 3647 . . . . . . . . . . . . . . . . . 18
7977, 78syl6sseq 3549 . . . . . . . . . . . . . . . . 17
80 ssundif 3911 . . . . . . . . . . . . . . . . 17
8179, 80sylib 196 . . . . . . . . . . . . . . . 16
82 simpr 461 . . . . . . . . . . . . . . . 16
83 fri 4846 . . . . . . . . . . . . . . . 16
8473, 76, 81, 82, 83syl22anc 1229 . . . . . . . . . . . . . . 15
85 brun 4500 . . . . . . . . . . . . . . . . . . . . . . 23
86 idd 24 . . . . . . . . . . . . . . . . . . . . . . . 24
87 brxp 5035 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8887simprbi 464 . . . . . . . . . . . . . . . . . . . . . . . . 25
89 eldifn 3626 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9089adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9190pm2.21d 106 . . . . . . . . . . . . . . . . . . . . . . . . 25
9288, 91syl5 32 . . . . . . . . . . . . . . . . . . . . . . . 24
9386, 92jaod 380 . . . . . . . . . . . . . . . . . . . . . . 23
9485, 93syl5bi 217 . . . . . . . . . . . . . . . . . . . . . 22
9594con3d 133 . . . . . . . . . . . . . . . . . . . . 21
9695ralimdv 2867 . . . . . . . . . . . . . . . . . . . 20
97 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23
9897ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22
9918ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . 24
10099ssbrd 4493 . . . . . . . . . . . . . . . . . . . . . . 23
101 brxp 5035 . . . . . . . . . . . . . . . . . . . . . . . 24
102101simplbi 460 . . . . . . . . . . . . . . . . . . . . . . 23
103100, 102syl6 33 . . . . . . . . . . . . . . . . . . . . . 22
10498, 103mtod 177 . . . . . . . . . . . . . . . . . . . . 21
105 brxp 5035 . . . . . . . . . . . . . . . . . . . . . . 23
106105simprbi 464 . . . . . . . . . . . . . . . . . . . . . 22
10790, 106nsyl 121 . . . . . . . . . . . . . . . . . . . . 21
108 brun 4500 . . . . . . . . . . . . . . . . . . . . . . . . 25
10963, 108syl6bb 261 . . . . . . . . . . . . . . . . . . . . . . . 24
110109notbid 294 . . . . . . . . . . . . . . . . . . . . . . 23
11146, 110ralsn 4068 . . . . . . . . . . . . . . . . . . . . . 22
112 ioran 490 . . . . . . . . . . . . . . . . . . . . . 22
113111, 112bitri 249 . . . . . . . . . . . . . . . . . . . . 21
114104, 107, 113sylanbrc 664 . . . . . . . . . . . . . . . . . . . 20
11596, 114jctird 544 . . . . . . . . . . . . . . . . . . 19
116 ssun1 3666 . . . . . . . . . . . . . . . . . . . . 21
117 undif1 3903 . . . . . . . . . . . . . . . . . . . . 21
118116, 117sseqtr4i 3536 . . . . . . . . . . . . . . . . . . . 20
119 ralun 3685 . . . . . . . . . . . . . . . . . . . 20
120 ssralv 3563 . . . . . . . . . . . . . . . . . . . 20
121118, 119, 120mpsyl 63 . . . . . . . . . . . . . . . . . . 19
122115, 121syl6 33 . . . . . . . . . . . . . . . . . 18
123 eldifi 3625 . . . . . . . . . . . . . . . . . . 19
124123adantl 466 . . . . . . . . . . . . . . . . . 18
125122, 124jctild 543 . . . . . . . . . . . . . . . . 17
126125expimpd 603 . . . . . . . . . . . . . . . 16
127126reximdv2 2928 . . . . . . . . . . . . . . 15
12884, 127mpd 15 . . . . . . . . . . . . . 14
129128ex 434 . . . . . . . . . . . . 13
13070, 129pm2.61dne 2774 . . . . . . . . . . . 12 <