Step Hyp Ref
Expression 1 df-rel 5011 . 2
2 dfss2 3492 . . . . 5
3 vex 3112 . . . . . . . . . 10
4 relop.1 . . . . . . . . . 10
5 relop.2 . . . . . . . . . 10
6 3 , 4 , 5 elop 4718 . . . . . . . . 9
7 elvv 5063 . . . . . . . . 9
8 6 , 7 imbi12i 326 . . . . . . . 8
9 jaob 783 . . . . . . . 8
10 8 , 9 bitri 249 . . . . . . 7
11 10 albii 1640 . . . . . 6
12 19.26 1680 . . . . . 6
13 11 , 12 bitri 249 . . . . 5
14 2 , 13 bitri 249 . . . 4
15 snex 4693 . . . . . . 7
16 eqeq1 2461 . . . . . . . 8
17 eqeq1 2461 . . . . . . . . . 10
18 eqcom 2466 . . . . . . . . . . 11
19 vex 3112 . . . . . . . . . . . 12
20 vex 3112 . . . . . . . . . . . 12
21 19 , 20 , 4 opeqsn 4748 . . . . . . . . . . 11
22 18 , 21 bitri 249 . . . . . . . . . 10
23 17 , 22 syl6bb 261 . . . . . . . . 9
24 23 2exbidv 1716 . . . . . . . 8
25 16 , 24 imbi12d 320 . . . . . . 7
26 15 , 25 spcv 3200 . . . . . 6
27 sneq 4039 . . . . . . . . 9
28 27 eqeq2d 2471 . . . . . . . 8
29 28 cbvexv 2024 . . . . . . 7
30 ax6ev 1749 . . . . . . . . . 10
31 equcom 1794 . . . . . . . . . . 11
32 31 exbii 1667 . . . . . . . . . 10
33 30 , 32 mpbi 208 . . . . . . . . 9
34 19.41v 1771 . . . . . . . . 9
35 33 , 34 mpbiran 918 . . . . . . . 8
36 35 exbii 1667 . . . . . . 7
37 eqid 2457 . . . . . . . 8
38 37 a1bi 337 . . . . . . 7
39 29 , 36 , 38 3bitr2ri 274 . . . . . 6
40 26 , 39 sylib 196 . . . . 5
41 eqid 2457 . . . . . 6
42 prex 4694 . . . . . . 7
43 eqeq1 2461 . . . . . . . 8
44 eqeq1 2461 . . . . . . . . 9
45 44 2exbidv 1716 . . . . . . . 8
46 43 , 45 imbi12d 320 . . . . . . 7
47 42 , 46 spcv 3200 . . . . . 6
48 41 , 47 mpi 17 . . . . 5
49 eqcom 2466 . . . . . . . . . 10
50 19 , 20 , 4 , 5 opeqpr 4749 . . . . . . . . . 10
51 49 , 50 bitri 249 . . . . . . . . 9
52 idd 24 . . . . . . . . . 10
53 eqtr2 2484 . . . . . . . . . . . . . 14
54 vex 3112 . . . . . . . . . . . . . . . 16
55 19 , 20 , 54 preqsn 4213 . . . . . . . . . . . . . . 15
56 55 simplbi 460 . . . . . . . . . . . . . 14
57 53 , 56 syl 16 . . . . . . . . . . . . 13
58 dfsn2 4042 . . . . . . . . . . . . . . . . . . . 20
59 preq2 4110 . . . . . . . . . . . . . . . . . . . 20
60 58 , 59 syl5req 2511 . . . . . . . . . . . . . . . . . . 19
61 60 eqeq2d 2471 . . . . . . . . . . . . . . . . . 18
62 58 , 59 syl5eq 2510 . . . . . . . . . . . . . . . . . . 19
63 62 eqeq2d 2471 . . . . . . . . . . . . . . . . . 18
64 61 , 63 anbi12d 710 . . . . . . . . . . . . . . . . 17
65 64 biimpd 207 . . . . . . . . . . . . . . . 16
66 65 expd 436 . . . . . . . . . . . . . . 15
67 66 com12 31 . . . . . . . . . . . . . 14
68 67 adantr 465 . . . . . . . . . . . . 13
69 57 , 68 mpd 15 . . . . . . . . . . . 12
70 69 expcom 435 . . . . . . . . . . 11
71 70 impd 431 . . . . . . . . . 10
72 52 , 71 jaod 380 . . . . . . . . 9
73 51 , 72 syl5bi 217 . . . . . . . 8
74 73 2eximdv 1712 . . . . . . 7
75 74 exlimiv 1722 . . . . . 6
76 75 imp 429 . . . . 5
77 40 , 48 , 76 syl2an 477 . . . 4
78 14 , 77 sylbi 195 . . 3
79 simpr 461 . . . . . . . . . . 11
80 equid 1791 . . . . . . . . . . . . . 14
81 80 jctl 541 . . . . . . . . . . . . 13
82 19 , 19 , 4 opeqsn 4748 . . . . . . . . . . . . 13
83 81 , 82 sylibr 212 . . . . . . . . . . . 12
84 83 adantr 465 . . . . . . . . . . 11
85 79 , 84 eqtr4d 2501 . . . . . . . . . 10
86 opeq12 4219 . . . . . . . . . . . 12
87 86 eqeq2d 2471 . . . . . . . . . . 11
88 19 , 19 , 87 spc2ev 3202 . . . . . . . . . 10
89 85 , 88 syl 16 . . . . . . . . 9
90 89 adantlr 714 . . . . . . . 8
91 preq12 4111 . . . . . . . . . . . 12
92 91 eqeq2d 2471 . . . . . . . . . . 11
93 92 biimpa 484 . . . . . . . . . 10
94 19 , 20 dfop 4216 . . . . . . . . . 10
95 93 , 94 syl6eqr 2516 . . . . . . . . 9
96 opeq12 4219 . . . . . . . . . . 11
97 96 eqeq2d 2471 . . . . . . . . . 10
98 19 , 20 , 97 spc2ev 3202 . . . . . . . . 9
99 95 , 98 syl 16 . . . . . . . 8
100 90 , 99 jaodan 785 . . . . . . 7
101 100 ex 434 . . . . . 6
102 elvv 5063 . . . . . 6
103 101 , 6 , 102 3imtr4g 270 . . . . 5
104 103 ssrdv 3509 . . . 4
105 104 exlimivv 1723 . . 3
106 78 , 105 impbii 188 . 2
107 1 , 106 bitri 249 1
