Metamath Proof Explorer


Theorem topdifinffinlem

Description: This is the core of the proof of topdifinffin , but to avoid the distinct variables on the definition, we need to split this proof into two. (Contributed by ML, 17-Jul-2020)

Ref Expression
Hypothesis topdifinf.t T = x 𝒫 A | ¬ A x Fin x = x = A
Assertion topdifinffinlem T TopOn A A Fin

Proof

Step Hyp Ref Expression
1 topdifinf.t T = x 𝒫 A | ¬ A x Fin x = x = A
2 nfv u ¬ A Fin
3 nfab1 _ u u | y A u = y
4 nfcv _ u T
5 abid u u | y A u = y y A u = y
6 df-rex y A u = y y y A u = y
7 5 6 bitri u u | y A u = y y y A u = y
8 eqid y = y
9 snex y V
10 snelpwi y A y 𝒫 A
11 eleq1 x = y x 𝒫 A y 𝒫 A
12 10 11 syl5ibr x = y y A x 𝒫 A
13 12 imdistani x = y y A x = y x 𝒫 A
14 13 anim2i ¬ A Fin x = y y A ¬ A Fin x = y x 𝒫 A
15 14 3impb ¬ A Fin x = y y A ¬ A Fin x = y x 𝒫 A
16 3anass ¬ A Fin x = y x 𝒫 A ¬ A Fin x = y x 𝒫 A
17 15 16 sylibr ¬ A Fin x = y y A ¬ A Fin x = y x 𝒫 A
18 snfi y Fin
19 eleq1 x = y x Fin y Fin
20 18 19 mpbiri x = y x Fin
21 difinf ¬ A Fin x Fin ¬ A x Fin
22 20 21 sylan2 ¬ A Fin x = y ¬ A x Fin
23 22 orcd ¬ A Fin x = y ¬ A x Fin x = x = A
24 23 anim2i x 𝒫 A ¬ A Fin x = y x 𝒫 A ¬ A x Fin x = x = A
25 24 ancoms ¬ A Fin x = y x 𝒫 A x 𝒫 A ¬ A x Fin x = x = A
26 25 3impa ¬ A Fin x = y x 𝒫 A x 𝒫 A ¬ A x Fin x = x = A
27 17 26 syl ¬ A Fin x = y y A x 𝒫 A ¬ A x Fin x = x = A
28 1 rabeq2i x T x 𝒫 A ¬ A x Fin x = x = A
29 27 28 sylibr ¬ A Fin x = y y A x T
30 eleq1 x = y x T y T
31 30 3ad2ant2 ¬ A Fin x = y y A x T y T
32 29 31 mpbid ¬ A Fin x = y y A y T
33 32 sbcth y V [˙ y / x]˙ ¬ A Fin x = y y A y T
34 9 33 ax-mp [˙ y / x]˙ ¬ A Fin x = y y A y T
35 sbcimg y V [˙ y / x]˙ ¬ A Fin x = y y A y T [˙ y / x]˙ ¬ A Fin x = y y A [˙ y / x]˙ y T
36 9 35 ax-mp [˙ y / x]˙ ¬ A Fin x = y y A y T [˙ y / x]˙ ¬ A Fin x = y y A [˙ y / x]˙ y T
37 34 36 mpbi [˙ y / x]˙ ¬ A Fin x = y y A [˙ y / x]˙ y T
38 sbc3an [˙ y / x]˙ ¬ A Fin x = y y A [˙ y / x]˙ ¬ A Fin [˙ y / x]˙ x = y [˙ y / x]˙ y A
39 sbcg y V [˙ y / x]˙ ¬ A Fin ¬ A Fin
40 9 39 ax-mp [˙ y / x]˙ ¬ A Fin ¬ A Fin
41 40 3anbi1i [˙ y / x]˙ ¬ A Fin [˙ y / x]˙ x = y [˙ y / x]˙ y A ¬ A Fin [˙ y / x]˙ x = y [˙ y / x]˙ y A
42 eqsbc3 y V [˙ y / x]˙ x = y y = y
43 9 42 ax-mp [˙ y / x]˙ x = y y = y
44 43 3anbi2i ¬ A Fin [˙ y / x]˙ x = y [˙ y / x]˙ y A ¬ A Fin y = y [˙ y / x]˙ y A
45 38 41 44 3bitri [˙ y / x]˙ ¬ A Fin x = y y A ¬ A Fin y = y [˙ y / x]˙ y A
46 sbcg y V [˙ y / x]˙ y A y A
47 9 46 ax-mp [˙ y / x]˙ y A y A
48 47 3anbi3i ¬ A Fin y = y [˙ y / x]˙ y A ¬ A Fin y = y y A
49 45 48 bitri [˙ y / x]˙ ¬ A Fin x = y y A ¬ A Fin y = y y A
50 sbcg y V [˙ y / x]˙ y T y T
51 9 50 ax-mp [˙ y / x]˙ y T y T
52 37 49 51 3imtr3i ¬ A Fin y = y y A y T
53 8 52 mp3an2 ¬ A Fin y A y T
54 53 ex ¬ A Fin y A y T
55 54 pm4.71d ¬ A Fin y A y A y T
56 55 anbi1d ¬ A Fin y A u = y y A y T u = y
57 56 exbidv ¬ A Fin y y A u = y y y A y T u = y
58 7 57 syl5bb ¬ A Fin u u | y A u = y y y A y T u = y
59 anass y A y T u = y y A y T u = y
60 59 exbii y y A y T u = y y y A y T u = y
61 exsimpr y y A y T u = y y y T u = y
62 60 61 sylbi y y A y T u = y y y T u = y
63 58 62 syl6bi ¬ A Fin u u | y A u = y y y T u = y
64 ancom y T u = y u = y y T
65 eleq1 u = y u T y T
66 65 pm5.32i u = y u T u = y y T
67 64 66 bitr4i y T u = y u = y u T
68 67 exbii y y T u = y y u = y u T
69 63 68 syl6ib ¬ A Fin u u | y A u = y y u = y u T
70 exsimpr y u = y u T y u T
71 69 70 syl6 ¬ A Fin u u | y A u = y y u T
72 ax5e y u T u T
73 71 72 syl6 ¬ A Fin u u | y A u = y u T
74 2 3 4 73 ssrd ¬ A Fin u | y A u = y T
75 eqid u | y A u = y = u | y A u = y
76 75 dissneq u | y A u = y T T TopOn A T = 𝒫 A
77 74 76 sylan ¬ A Fin T TopOn A T = 𝒫 A
78 nfielex ¬ A Fin y y A
79 78 adantr ¬ A Fin T TopOn A y y A
80 difss A y A
81 elfvex T TopOn A A V
82 difexg A V A y V
83 elpwg A y V A y 𝒫 A A y A
84 81 82 83 3syl T TopOn A A y 𝒫 A A y A
85 80 84 mpbiri T TopOn A A y 𝒫 A
86 85 adantl ¬ A Fin T TopOn A A y 𝒫 A
87 difinf ¬ A Fin y Fin ¬ A y Fin
88 18 87 mpan2 ¬ A Fin ¬ A y Fin
89 0fin Fin
90 eleq1 A y = A y Fin Fin
91 89 90 mpbiri A y = A y Fin
92 88 91 nsyl ¬ A Fin ¬ A y =
93 92 ad2antrl y A ¬ A Fin T TopOn A ¬ A y =
94 vsnid y y
95 inelcm y A y y A y
96 94 95 mpan2 y A A y
97 disj4 A y = ¬ A y A
98 97 necon2abii A y A A y
99 96 98 sylibr y A A y A
100 99 pssned y A A y A
101 100 adantr y A ¬ A Fin T TopOn A A y A
102 101 neneqd y A ¬ A Fin T TopOn A ¬ A y = A
103 93 102 jca y A ¬ A Fin T TopOn A ¬ A y = ¬ A y = A
104 pm4.56 ¬ A y = ¬ A y = A ¬ A y = A y = A
105 103 104 sylib y A ¬ A Fin T TopOn A ¬ A y = A y = A
106 difeq2 x = A y A x = A A y
107 106 eleq1d x = A y A x Fin A A y Fin
108 107 notbid x = A y ¬ A x Fin ¬ A A y Fin
109 eqeq1 x = A y x = A y =
110 eqeq1 x = A y x = A A y = A
111 109 110 orbi12d x = A y x = x = A A y = A y = A
112 108 111 orbi12d x = A y ¬ A x Fin x = x = A ¬ A A y Fin A y = A y = A
113 112 1 elrab2 A y T A y 𝒫 A ¬ A A y Fin A y = A y = A
114 85 biantrurd T TopOn A ¬ A A y Fin A y = A y = A A y 𝒫 A ¬ A A y Fin A y = A y = A
115 113 114 bitr4id T TopOn A A y T ¬ A A y Fin A y = A y = A
116 dfin4 A y = A A y
117 inss2 A y y
118 ssfi y Fin A y y A y Fin
119 18 117 118 mp2an A y Fin
120 116 119 eqeltrri A A y Fin
121 biortn A A y Fin A y = A y = A ¬ A A y Fin A y = A y = A
122 120 121 ax-mp A y = A y = A ¬ A A y Fin A y = A y = A
123 115 122 bitr4di T TopOn A A y T A y = A y = A
124 123 ad2antll y A ¬ A Fin T TopOn A A y T A y = A y = A
125 105 124 mtbird y A ¬ A Fin T TopOn A ¬ A y T
126 125 expcom ¬ A Fin T TopOn A y A ¬ A y T
127 nelneq2 A y 𝒫 A ¬ A y T ¬ 𝒫 A = T
128 eqcom T = 𝒫 A 𝒫 A = T
129 127 128 sylnibr A y 𝒫 A ¬ A y T ¬ T = 𝒫 A
130 86 126 129 syl6an ¬ A Fin T TopOn A y A ¬ T = 𝒫 A
131 79 130 exellimddv ¬ A Fin T TopOn A ¬ T = 𝒫 A
132 77 131 pm2.65da ¬ A Fin ¬ T TopOn A
133 132 con4i T TopOn A A Fin