Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . 3
|
2 | | 1sdom 8163 |
. . 3
|
3 | 1, 2 | ax-mp 5 |
. 2
|
4 | | vex 3203 |
. . 3
|
5 | | 1sdom 8163 |
. . 3
|
6 | 4, 5 | ax-mp 5 |
. 2
|
7 | | reeanv 3107 |
. . 3
|
8 | | reeanv 3107 |
. . . . 5
|
9 | | unxpdomlem1.2 |
. . . . . . . . . . 11
|
10 | | simpr 477 |
. . . . . . . . . . . . 13
|
11 | | simp2r 1088 |
. . . . . . . . . . . . . . 15
|
12 | | simp1r 1086 |
. . . . . . . . . . . . . . 15
|
13 | 11, 12 | ifcld 4131 |
. . . . . . . . . . . . . 14
|
14 | 13 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
15 | | opelxpi 5148 |
. . . . . . . . . . . . 13
|
16 | 10, 14, 15 | syl2anc 693 |
. . . . . . . . . . . 12
|
17 | | simp2l 1087 |
. . . . . . . . . . . . . . 15
|
18 | | simp1l 1085 |
. . . . . . . . . . . . . . 15
|
19 | 17, 18 | ifcld 4131 |
. . . . . . . . . . . . . 14
|
20 | 19 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
21 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
22 | | elun 3753 |
. . . . . . . . . . . . . . 15
|
23 | 21, 22 | sylib 208 |
. . . . . . . . . . . . . 14
|
24 | 23 | orcanai 952 |
. . . . . . . . . . . . 13
|
25 | | opelxpi 5148 |
. . . . . . . . . . . . 13
|
26 | 20, 24, 25 | syl2anc 693 |
. . . . . . . . . . . 12
|
27 | 16, 26 | ifclda 4120 |
. . . . . . . . . . 11
|
28 | 9, 27 | syl5eqel 2705 |
. . . . . . . . . 10
|
29 | | unxpdomlem1.1 |
. . . . . . . . . 10
|
30 | 28, 29 | fmptd 6385 |
. . . . . . . . 9
|
31 | 29, 9 | unxpdomlem1 8164 |
. . . . . . . . . . . . . . . 16
|
32 | 31 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
|
33 | | iftrue 4092 |
. . . . . . . . . . . . . . . 16
|
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . 15
|
35 | 32, 34 | sylan9eq 2676 |
. . . . . . . . . . . . . 14
|
36 | 29, 9 | unxpdomlem1 8164 |
. . . . . . . . . . . . . . . 16
|
37 | 36 | ad2antll 765 |
. . . . . . . . . . . . . . 15
|
38 | | iftrue 4092 |
. . . . . . . . . . . . . . . 16
|
39 | 38 | adantl 482 |
. . . . . . . . . . . . . . 15
|
40 | 37, 39 | sylan9eq 2676 |
. . . . . . . . . . . . . 14
|
41 | 35, 40 | eqeq12d 2637 |
. . . . . . . . . . . . 13
|
42 | | vex 3203 |
. . . . . . . . . . . . . 14
|
43 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
44 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
45 | 43, 44 | ifex 4156 |
. . . . . . . . . . . . . 14
|
46 | 42, 45 | opth1 4944 |
. . . . . . . . . . . . 13
|
47 | 41, 46 | syl6bi 243 |
. . . . . . . . . . . 12
|
48 | | simprr 796 |
. . . . . . . . . . . . . 14
|
49 | | simpll 790 |
. . . . . . . . . . . . . 14
|
50 | | simplr 792 |
. . . . . . . . . . . . . 14
|
51 | 29, 9, 48, 49, 50 | unxpdomlem2 8165 |
. . . . . . . . . . . . 13
|
52 | 51 | pm2.21d 118 |
. . . . . . . . . . . 12
|
53 | | eqcom 2629 |
. . . . . . . . . . . . 13
|
54 | | simprl 794 |
. . . . . . . . . . . . . . . 16
|
55 | 29, 9, 54, 49, 50 | unxpdomlem2 8165 |
. . . . . . . . . . . . . . 15
|
56 | 55 | ancom2s 844 |
. . . . . . . . . . . . . 14
|
57 | 56 | pm2.21d 118 |
. . . . . . . . . . . . 13
|
58 | 53, 57 | syl5bi 232 |
. . . . . . . . . . . 12
|
59 | | iffalse 4095 |
. . . . . . . . . . . . . . . 16
|
60 | 59 | adantr 481 |
. . . . . . . . . . . . . . 15
|
61 | 32, 60 | sylan9eq 2676 |
. . . . . . . . . . . . . 14
|
62 | | iffalse 4095 |
. . . . . . . . . . . . . . . 16
|
63 | 62 | adantl 482 |
. . . . . . . . . . . . . . 15
|
64 | 37, 63 | sylan9eq 2676 |
. . . . . . . . . . . . . 14
|
65 | 61, 64 | eqeq12d 2637 |
. . . . . . . . . . . . 13
|
66 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
67 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
68 | 66, 67 | ifex 4156 |
. . . . . . . . . . . . . . 15
|
69 | 68, 42 | opth 4945 |
. . . . . . . . . . . . . 14
|
70 | 69 | simprbi 480 |
. . . . . . . . . . . . 13
|
71 | 65, 70 | syl6bi 243 |
. . . . . . . . . . . 12
|
72 | 47, 52, 58, 71 | 4casesdan 991 |
. . . . . . . . . . 11
|
73 | 72 | ralrimivva 2971 |
. . . . . . . . . 10
|
74 | 73 | 3ad2ant3 1084 |
. . . . . . . . 9
|
75 | | dff13 6512 |
. . . . . . . . 9
|
76 | 30, 74, 75 | sylanbrc 698 |
. . . . . . . 8
|
77 | 1, 4 | unex 6956 |
. . . . . . . . 9
|
78 | 1, 4 | xpex 6962 |
. . . . . . . . 9
|
79 | | f1dom2g 7973 |
. . . . . . . . 9
|
80 | 77, 78, 79 | mp3an12 1414 |
. . . . . . . 8
|
81 | 76, 80 | syl 17 |
. . . . . . 7
|
82 | 81 | 3expia 1267 |
. . . . . 6
|
83 | 82 | rexlimdvva 3038 |
. . . . 5
|
84 | 8, 83 | syl5bir 233 |
. . . 4
|
85 | 84 | rexlimivv 3036 |
. . 3
|
86 | 7, 85 | sylbir 225 |
. 2
|
87 | 3, 6, 86 | syl2anb 496 |
1
|