Step | Hyp | Ref
| Expression |
1 | | indf1o 28838 |
. . . 4
 𝟭              |
2 | | f1of1 5811 |
. . . 4
 𝟭            𝟭              |
3 | 1, 2 | syl 17 |
. . 3
 𝟭              |
4 | | inss1 3651 |
. . 3
     |
5 | | f1ores 5826 |
. . 3
  𝟭                  𝟭              𝟭          |
6 | 3, 4, 5 | sylancl 667 |
. 2
  𝟭              𝟭          |
7 | | resres 5116 |
. . . 4
  𝟭    
 𝟭       |
8 | | f1ofn 5813 |
. . . . . 6
 𝟭            𝟭     |
9 | | fnresdm 5683 |
. . . . . 6
 𝟭    𝟭    𝟭    |
10 | 1, 8, 9 | 3syl 18 |
. . . . 5
  𝟭    𝟭    |
11 | 10 | reseq1d 5103 |
. . . 4
   𝟭    
 𝟭     |
12 | 7, 11 | syl5eqr 2498 |
. . 3
  𝟭       𝟭     |
13 | | eqidd 2451 |
. . 3
  
      |
14 | | simpll 759 |
. . . . . . . . . 10
  
 
 
 𝟭        |
15 | | simpr 463 |
. . . . . . . . . . . . . . 15
 
         |
16 | 4, 15 | sseldi 3429 |
. . . . . . . . . . . . . 14
 
       |
17 | 16 | elpwid 3960 |
. . . . . . . . . . . . 13
 
      |
18 | | indf 28830 |
. . . . . . . . . . . . 13
    𝟭              |
19 | 17, 18 | syldan 473 |
. . . . . . . . . . . 12
 
     𝟭              |
20 | 19 | adantr 467 |
. . . . . . . . . . 11
  
 
 
 𝟭       𝟭              |
21 | | simpr 463 |
. . . . . . . . . . . 12
  
 
 
 𝟭       𝟭       |
22 | 21 | feq1d 5712 |
. . . . . . . . . . 11
  
 
 
 𝟭        𝟭           
          |
23 | 20, 22 | mpbid 214 |
. . . . . . . . . 10
  
 
 
 𝟭               |
24 | | prex 4641 |
. . . . . . . . . . . 12
    |
25 | | elmapg 7482 |
. . . . . . . . . . . 12
    
                 |
26 | 24, 25 | mpan 675 |
. . . . . . . . . . 11
      
          |
27 | 26 | biimpar 488 |
. . . . . . . . . 10
                 |
28 | 14, 23, 27 | syl2anc 666 |
. . . . . . . . 9
  
 
 
 𝟭             |
29 | 21 | cnveqd 5009 |
. . . . . . . . . . 11
  
 
 
 𝟭        𝟭        |
30 | 29 | imaeq1d 5166 |
. . . . . . . . . 10
  
 
 
 𝟭         𝟭                   |
31 | | indpi1 28836 |
. . . . . . . . . . . . 13
      𝟭            |
32 | 17, 31 | syldan 473 |
. . . . . . . . . . . 12
 
       𝟭            |
33 | | inss2 3652 |
. . . . . . . . . . . . 13
    |
34 | 33, 15 | sseldi 3429 |
. . . . . . . . . . . 12
 
      |
35 | 32, 34 | eqeltrd 2528 |
. . . . . . . . . . 11
 
       𝟭            |
36 | 35 | adantr 467 |
. . . . . . . . . 10
  
 
 
 𝟭         𝟭            |
37 | 30, 36 | eqeltrrd 2529 |
. . . . . . . . 9
  
 
 
 𝟭               |
38 | 28, 37 | jca 535 |
. . . . . . . 8
  
 
 
 𝟭           
          |
39 | 38 | ex 436 |
. . . . . . 7
 
      𝟭                      |
40 | 39 | rexlimdva 2878 |
. . . . . 6
  
 
   𝟭          
           |
41 | | cnvimass 5187 |
. . . . . . . . . 10
        |
42 | 26 | biimpa 487 |
. . . . . . . . . . . 12
 
               |
43 | | fdm 5731 |
. . . . . . . . . . . 12
          |
44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
 
     
  |
45 | 44 | adantrr 722 |
. . . . . . . . . 10
                
  |
46 | 41, 45 | syl5sseq 3479 |
. . . . . . . . 9
                
      
  |
47 | | simprr 765 |
. . . . . . . . 9
                
         |
48 | | elfpw 7873 |
. . . . . . . . 9
                             |
49 | 46, 47, 48 | sylanbrc 669 |
. . . . . . . 8
                
            |
50 | | indpreima 28839 |
. . . . . . . . . . 11
           𝟭              |
51 | 50 | eqcomd 2456 |
. . . . . . . . . 10
           𝟭              |
52 | 42, 51 | syldan 473 |
. . . . . . . . 9
 
       𝟭              |
53 | 52 | adantrr 722 |
. . . . . . . 8
                
 𝟭              |
54 | | fveq2 5863 |
. . . . . . . . . 10
       
 𝟭      𝟭              |
55 | 54 | eqeq1d 2452 |
. . . . . . . . 9
       
  𝟭      𝟭               |
56 | 55 | rspcev 3149 |
. . . . . . . 8
             𝟭             
 
   𝟭       |
57 | 49, 53, 56 | syl2anc 666 |
. . . . . . 7
                
      𝟭       |
58 | 57 | ex 436 |
. . . . . 6
                      𝟭        |
59 | 40, 58 | impbid 194 |
. . . . 5
  
 
   𝟭                      |
60 | 1, 8 | syl 17 |
. . . . . 6
 𝟭     |
61 | | fvelimab 5919 |
. . . . . 6
  𝟭    
     𝟭       
      𝟭        |
62 | 60, 4, 61 | sylancl 667 |
. . . . 5
   𝟭     
        𝟭        |
63 | | cnveq 5007 |
. . . . . . . . 9
 
   |
64 | 63 | imaeq1d 5166 |
. . . . . . . 8
                 |
65 | 64 | eleq1d 2512 |
. . . . . . 7
        
          |
66 | 65 | elrab 3195 |
. . . . . 6
                               |
67 | 66 | a1i 11 |
. . . . 5
               
     
           |
68 | 59, 62, 67 | 3bitr4d 289 |
. . . 4
   𝟭     
                   |
69 | 68 | eqrdv 2448 |
. . 3
  𝟭                        |
70 | 12, 13, 69 | f1oeq123d 5809 |
. 2
   𝟭              𝟭       
 𝟭                           |
71 | 6, 70 | mpbid 214 |
1
  𝟭                          |