Metamath Proof Explorer


Theorem elrfi

Description: Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion elrfi B V C 𝒫 B A fi B C v 𝒫 C Fin A = B v

Proof

Step Hyp Ref Expression
1 elex A fi B C A V
2 1 a1i B V C 𝒫 B A fi B C A V
3 inex1g B V B v V
4 eleq1 A = B v A V B v V
5 3 4 syl5ibrcom B V A = B v A V
6 5 rexlimdvw B V v 𝒫 C Fin A = B v A V
7 6 adantr B V C 𝒫 B v 𝒫 C Fin A = B v A V
8 simpr B V C 𝒫 B A V A V
9 snex B V
10 pwexg B V 𝒫 B V
11 10 ad2antrr B V C 𝒫 B A V 𝒫 B V
12 simplr B V C 𝒫 B A V C 𝒫 B
13 11 12 ssexd B V C 𝒫 B A V C V
14 unexg B V C V B C V
15 9 13 14 sylancr B V C 𝒫 B A V B C V
16 elfi A V B C V A fi B C w 𝒫 B C Fin A = w
17 8 15 16 syl2anc B V C 𝒫 B A V A fi B C w 𝒫 B C Fin A = w
18 inss1 𝒫 B C Fin 𝒫 B C
19 uncom B C = C B
20 19 pweqi 𝒫 B C = 𝒫 C B
21 18 20 sseqtri 𝒫 B C Fin 𝒫 C B
22 21 sseli w 𝒫 B C Fin w 𝒫 C B
23 9 elpwun w 𝒫 C B w B 𝒫 C
24 22 23 sylib w 𝒫 B C Fin w B 𝒫 C
25 24 ad2antrl B V C 𝒫 B A V w 𝒫 B C Fin A = w w B 𝒫 C
26 inss2 𝒫 B C Fin Fin
27 26 sseli w 𝒫 B C Fin w Fin
28 diffi w Fin w B Fin
29 27 28 syl w 𝒫 B C Fin w B Fin
30 29 ad2antrl B V C 𝒫 B A V w 𝒫 B C Fin A = w w B Fin
31 25 30 elind B V C 𝒫 B A V w 𝒫 B C Fin A = w w B 𝒫 C Fin
32 incom B A = A B
33 simprr B V C 𝒫 B A V w 𝒫 B C Fin A = w A = w
34 simplr B V C 𝒫 B A V w 𝒫 B C Fin A = w A V
35 33 34 eqeltrrd B V C 𝒫 B A V w 𝒫 B C Fin A = w w V
36 intex w w V
37 35 36 sylibr B V C 𝒫 B A V w 𝒫 B C Fin A = w w
38 intssuni w w w
39 37 38 syl B V C 𝒫 B A V w 𝒫 B C Fin A = w w w
40 18 sseli w 𝒫 B C Fin w 𝒫 B C
41 40 elpwid w 𝒫 B C Fin w B C
42 41 ad2antrl B V C 𝒫 B A V w 𝒫 B C Fin A = w w B C
43 pwidg B V B 𝒫 B
44 43 snssd B V B 𝒫 B
45 44 adantr B V C 𝒫 B B 𝒫 B
46 simpr B V C 𝒫 B C 𝒫 B
47 45 46 unssd B V C 𝒫 B B C 𝒫 B
48 47 ad2antrr B V C 𝒫 B A V w 𝒫 B C Fin A = w B C 𝒫 B
49 42 48 sstrd B V C 𝒫 B A V w 𝒫 B C Fin A = w w 𝒫 B
50 sspwuni w 𝒫 B w B
51 49 50 sylib B V C 𝒫 B A V w 𝒫 B C Fin A = w w B
52 39 51 sstrd B V C 𝒫 B A V w 𝒫 B C Fin A = w w B
53 33 52 eqsstrd B V C 𝒫 B A V w 𝒫 B C Fin A = w A B
54 df-ss A B A B = A
55 53 54 sylib B V C 𝒫 B A V w 𝒫 B C Fin A = w A B = A
56 32 55 eqtr2id B V C 𝒫 B A V w 𝒫 B C Fin A = w A = B A
57 ineq2 A = w B A = B w
58 57 ad2antll B V C 𝒫 B A V w 𝒫 B C Fin A = w B A = B w
59 56 58 eqtrd B V C 𝒫 B A V w 𝒫 B C Fin A = w A = B w
60 intun B w = B w
61 intsng B V B = B
62 61 ineq1d B V B w = B w
63 60 62 eqtr2id B V B w = B w
64 63 ad3antrrr B V C 𝒫 B A V w 𝒫 B C Fin A = w B w = B w
65 59 64 eqtrd B V C 𝒫 B A V w 𝒫 B C Fin A = w A = B w
66 undif2 B w B = B w
67 66 inteqi B w B = B w
68 65 67 eqtr4di B V C 𝒫 B A V w 𝒫 B C Fin A = w A = B w B
69 intun B w B = B w B
70 61 ineq1d B V B w B = B w B
71 69 70 syl5eq B V B w B = B w B
72 71 ad3antrrr B V C 𝒫 B A V w 𝒫 B C Fin A = w B w B = B w B
73 68 72 eqtrd B V C 𝒫 B A V w 𝒫 B C Fin A = w A = B w B
74 inteq v = w B v = w B
75 74 ineq2d v = w B B v = B w B
76 75 rspceeqv w B 𝒫 C Fin A = B w B v 𝒫 C Fin A = B v
77 31 73 76 syl2anc B V C 𝒫 B A V w 𝒫 B C Fin A = w v 𝒫 C Fin A = B v
78 77 rexlimdvaa B V C 𝒫 B A V w 𝒫 B C Fin A = w v 𝒫 C Fin A = B v
79 ssun1 B B C
80 79 a1i B V C 𝒫 B A V v 𝒫 C Fin B B C
81 inss1 𝒫 C Fin 𝒫 C
82 81 sseli v 𝒫 C Fin v 𝒫 C
83 elpwi v 𝒫 C v C
84 ssun4 v C v B C
85 82 83 84 3syl v 𝒫 C Fin v B C
86 85 adantl B V C 𝒫 B A V v 𝒫 C Fin v B C
87 80 86 unssd B V C 𝒫 B A V v 𝒫 C Fin B v B C
88 vex v V
89 9 88 unex B v V
90 89 elpw B v 𝒫 B C B v B C
91 87 90 sylibr B V C 𝒫 B A V v 𝒫 C Fin B v 𝒫 B C
92 snfi B Fin
93 inss2 𝒫 C Fin Fin
94 93 sseli v 𝒫 C Fin v Fin
95 94 adantl B V C 𝒫 B A V v 𝒫 C Fin v Fin
96 unfi B Fin v Fin B v Fin
97 92 95 96 sylancr B V C 𝒫 B A V v 𝒫 C Fin B v Fin
98 91 97 elind B V C 𝒫 B A V v 𝒫 C Fin B v 𝒫 B C Fin
99 61 eqcomd B V B = B
100 99 ineq1d B V B v = B v
101 intun B v = B v
102 100 101 eqtr4di B V B v = B v
103 102 ad3antrrr B V C 𝒫 B A V v 𝒫 C Fin B v = B v
104 inteq w = B v w = B v
105 104 rspceeqv B v 𝒫 B C Fin B v = B v w 𝒫 B C Fin B v = w
106 98 103 105 syl2anc B V C 𝒫 B A V v 𝒫 C Fin w 𝒫 B C Fin B v = w
107 eqeq1 A = B v A = w B v = w
108 107 rexbidv A = B v w 𝒫 B C Fin A = w w 𝒫 B C Fin B v = w
109 106 108 syl5ibrcom B V C 𝒫 B A V v 𝒫 C Fin A = B v w 𝒫 B C Fin A = w
110 109 rexlimdva B V C 𝒫 B A V v 𝒫 C Fin A = B v w 𝒫 B C Fin A = w
111 78 110 impbid B V C 𝒫 B A V w 𝒫 B C Fin A = w v 𝒫 C Fin A = B v
112 17 111 bitrd B V C 𝒫 B A V A fi B C v 𝒫 C Fin A = B v
113 112 ex B V C 𝒫 B A V A fi B C v 𝒫 C Fin A = B v
114 2 7 113 pm5.21ndd B V C 𝒫 B A fi B C v 𝒫 C Fin A = B v