Step | Hyp | Ref
| Expression |
1 | | df-afs 30748 |
. . 3
AFS TarskiG
Itv
|
2 | 1 | a1i 11 |
. 2
AFS TarskiG
Itv
|
3 | | brafs.p |
. . . . 5
|
4 | | brafs.d |
. . . . 5
|
5 | | brafs.i |
. . . . 5
Itv |
6 | | simp1 1061 |
. . . . . . 7
|
7 | 6 | eqcomd 2628 |
. . . . . 6
|
8 | 7 | adantr 481 |
. . . . . . 7
|
9 | 8 | adantr 481 |
. . . . . . . 8
|
10 | 9 | adantr 481 |
. . . . . . . . 9
|
11 | 10 | adantr 481 |
. . . . . . . . . 10
|
12 | 11 | adantr 481 |
. . . . . . . . . . 11
|
13 | 12 | adantr 481 |
. . . . . . . . . . . 12
|
14 | 7 | ad7antr 774 |
. . . . . . . . . . . . 13
|
15 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . 20
|
16 | 15 | ad8antr 776 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 16 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
|
18 | 17 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
19 | 18 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
|
20 | 17 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
21 | 20 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
|
22 | 19, 21 | anbi12d 747 |
. . . . . . . . . . . . . . 15
|
23 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . 20
|
24 | 23 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . 19
|
25 | 24 | ad8antr 776 |
. . . . . . . . . . . . . . . . . 18
|
26 | 25 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
27 | 25 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
28 | 26, 27 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
29 | 25 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
30 | 25 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
31 | 29, 30 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
32 | 28, 31 | anbi12d 747 |
. . . . . . . . . . . . . . 15
|
33 | 25 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
34 | 25 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
35 | 33, 34 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
36 | 25 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
37 | 25 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
38 | 36, 37 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
39 | 35, 38 | anbi12d 747 |
. . . . . . . . . . . . . . 15
|
40 | 22, 32, 39 | 3anbi123d 1399 |
. . . . . . . . . . . . . 14
|
41 | 40 | 3anbi3d 1405 |
. . . . . . . . . . . . 13
|
42 | 14, 41 | rexeqbidva 3155 |
. . . . . . . . . . . 12
|
43 | 13, 42 | rexeqbidva 3155 |
. . . . . . . . . . 11
|
44 | 12, 43 | rexeqbidva 3155 |
. . . . . . . . . 10
|
45 | 11, 44 | rexeqbidva 3155 |
. . . . . . . . 9
|
46 | 10, 45 | rexeqbidva 3155 |
. . . . . . . 8
|
47 | 9, 46 | rexeqbidva 3155 |
. . . . . . 7
|
48 | 8, 47 | rexeqbidva 3155 |
. . . . . 6
|
49 | 7, 48 | rexeqbidva 3155 |
. . . . 5
|
50 | 3, 4, 5, 49 | sbcie3s 15917 |
. . . 4
Itv
|
51 | 50 | adantl 482 |
. . 3
Itv
|
52 | 51 | opabbidv 4716 |
. 2
Itv
|
53 | | brafs.g |
. 2
TarskiG |
54 | | df-xp 5120 |
. . . . 5
|
55 | | fvex 6201 |
. . . . . . . . 9
|
56 | 3, 55 | eqeltri 2697 |
. . . . . . . 8
|
57 | 56, 56 | xpex 6962 |
. . . . . . 7
|
58 | 57, 57 | xpex 6962 |
. . . . . 6
|
59 | 58, 58 | xpex 6962 |
. . . . 5
|
60 | 54, 59 | eqeltrri 2698 |
. . . 4
|
61 | | 3simpa 1058 |
. . . . . . . . . . . . . 14
|
62 | 61 | reximi 3011 |
. . . . . . . . . . . . 13
|
63 | 62 | reximi 3011 |
. . . . . . . . . . . 12
|
64 | 63 | reximi 3011 |
. . . . . . . . . . 11
|
65 | 64 | reximi 3011 |
. . . . . . . . . 10
|
66 | 65 | reximi 3011 |
. . . . . . . . 9
|
67 | 66 | reximi 3011 |
. . . . . . . 8
|
68 | 67 | reximi 3011 |
. . . . . . 7
|
69 | 68 | reximi 3011 |
. . . . . 6
|
70 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
71 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . 18
|
72 | 71 | ad7antr 774 |
. . . . . . . . . . . . . . . . 17
|
73 | | simp-7r 813 |
. . . . . . . . . . . . . . . . . 18
|
74 | | simp-6r 811 |
. . . . . . . . . . . . . . . . . 18
|
75 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . 18
|
76 | 73, 74, 75 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
77 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . 17
|
78 | 72, 76, 77 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
79 | 70, 78 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
|
80 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
81 | | simp-5r 809 |
. . . . . . . . . . . . . . . . . 18
|
82 | | simp-4r 807 |
. . . . . . . . . . . . . . . . . 18
|
83 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . 18
|
84 | 81, 82, 83 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
85 | | simpllr 799 |
. . . . . . . . . . . . . . . . . 18
|
86 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
|
87 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . 18
|
88 | 85, 86, 87 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
89 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . 17
|
90 | 84, 88, 89 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
91 | 80, 90 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
|
92 | 79, 91 | anim12dan 882 |
. . . . . . . . . . . . . 14
|
93 | 92 | ex 450 |
. . . . . . . . . . . . 13
|
94 | 93 | rexlimdva 3031 |
. . . . . . . . . . . 12
|
95 | 94 | rexlimdva 3031 |
. . . . . . . . . . 11
|
96 | 95 | rexlimdva 3031 |
. . . . . . . . . 10
|
97 | 96 | rexlimdva 3031 |
. . . . . . . . 9
|
98 | 97 | rexlimdva 3031 |
. . . . . . . 8
|
99 | 98 | rexlimdva 3031 |
. . . . . . 7
|
100 | 99 | rexlimivv 3036 |
. . . . . 6
|
101 | 69, 100 | syl 17 |
. . . . 5
|
102 | 101 | ssopab2i 5003 |
. . . 4
|
103 | 60, 102 | ssexi 4803 |
. . 3
|
104 | 103 | a1i 11 |
. 2
|
105 | 2, 52, 53, 104 | fvmptd 6288 |
1
AFS
|