Step | Hyp | Ref
| Expression |
1 | | unirnmapsn.C |
. . . . 5
|
2 | | snex 4908 |
. . . . 5
|
3 | 1, 2 | eqeltri 2697 |
. . . 4
|
4 | 3 | a1i 11 |
. . 3
|
5 | | unirnmapsn.x |
. . 3
|
6 | 4, 5 | unirnmap 39400 |
. 2
|
7 | | simpl 473 |
. . . . . 6
|
8 | | equid 1939 |
. . . . . . . . 9
|
9 | | rnuni 5544 |
. . . . . . . . . 10
|
10 | 9 | oveq1i 6660 |
. . . . . . . . 9
|
11 | 8, 10 | eleq12i 2694 |
. . . . . . . 8
|
12 | 11 | biimpi 206 |
. . . . . . 7
|
13 | 12 | adantl 482 |
. . . . . 6
|
14 | | ovexd 6680 |
. . . . . . . . . . . 12
|
15 | 14, 5 | ssexd 4805 |
. . . . . . . . . . 11
|
16 | | rnexg 7098 |
. . . . . . . . . . . . 13
|
17 | 16 | rgen 2922 |
. . . . . . . . . . . 12
|
18 | 17 | a1i 11 |
. . . . . . . . . . 11
|
19 | | iunexg 7143 |
. . . . . . . . . . 11
|
20 | 15, 18, 19 | syl2anc 693 |
. . . . . . . . . 10
|
21 | 20, 4 | elmapd 7871 |
. . . . . . . . 9
|
22 | 21 | biimpa 501 |
. . . . . . . 8
|
23 | | unirnmapsn.A |
. . . . . . . . . . 11
|
24 | | snidg 4206 |
. . . . . . . . . . 11
|
25 | 23, 24 | syl 17 |
. . . . . . . . . 10
|
26 | 25, 1 | syl6eleqr 2712 |
. . . . . . . . 9
|
27 | 26 | adantr 481 |
. . . . . . . 8
|
28 | 22, 27 | ffvelrnd 6360 |
. . . . . . 7
|
29 | | eliun 4524 |
. . . . . . 7
|
30 | 28, 29 | sylib 208 |
. . . . . 6
|
31 | 7, 13, 30 | syl2anc 693 |
. . . . 5
|
32 | | elmapfn 7880 |
. . . . . . . 8
|
33 | 32 | adantl 482 |
. . . . . . 7
|
34 | | simp3 1063 |
. . . . . . . . . . . . 13
|
35 | 23 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
|
36 | 1 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 5, 36 | syl6sseq 3651 |
. . . . . . . . . . . . . . . . . 18
|
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
39 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
40 | 38, 39 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
|
41 | | unirnmapsn.b |
. . . . . . . . . . . . . . . . . 18
|
42 | 41 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
43 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
44 | 42, 43 | elmapd 7871 |
. . . . . . . . . . . . . . . 16
|
45 | 40, 44 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
46 | 45 | 3adant3 1081 |
. . . . . . . . . . . . . 14
|
47 | 35, 46 | rnsnf 39370 |
. . . . . . . . . . . . 13
|
48 | 34, 47 | eleqtrd 2703 |
. . . . . . . . . . . 12
|
49 | | fvex 6201 |
. . . . . . . . . . . . 13
|
50 | 49 | elsn 4192 |
. . . . . . . . . . . 12
|
51 | 48, 50 | sylib 208 |
. . . . . . . . . . 11
|
52 | 51 | 3adant1r 1319 |
. . . . . . . . . 10
|
53 | 23 | adantr 481 |
. . . . . . . . . . . 12
|
54 | 53 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
55 | | simp1r 1086 |
. . . . . . . . . . 11
|
56 | 40, 36 | syl6eleqr 2712 |
. . . . . . . . . . . . . 14
|
57 | | elmapfn 7880 |
. . . . . . . . . . . . . 14
|
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . 13
|
59 | 58 | adantlr 751 |
. . . . . . . . . . . 12
|
60 | 59 | 3adant3 1081 |
. . . . . . . . . . 11
|
61 | 54, 1, 55, 60 | fsneq 39398 |
. . . . . . . . . 10
|
62 | 52, 61 | mpbird 247 |
. . . . . . . . 9
|
63 | | simp2 1062 |
. . . . . . . . 9
|
64 | 62, 63 | eqeltrd 2701 |
. . . . . . . 8
|
65 | 64 | 3exp 1264 |
. . . . . . 7
|
66 | 7, 33, 65 | syl2anc 693 |
. . . . . 6
|
67 | 66 | rexlimdv 3030 |
. . . . 5
|
68 | 31, 67 | mpd 15 |
. . . 4
|
69 | 68 | ralrimiva 2966 |
. . 3
|
70 | | dfss3 3592 |
. . 3
|
71 | 69, 70 | sylibr 224 |
. 2
|
72 | 6, 71 | eqssd 3620 |
1
|