Table of ContentsTable of Contents Mathbox for Jeff Hankins < Previous   Next >
Related theorems
Unicode version
Theorem alexsublem4 15440
Description: Lemma for alexsub 15441. If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover.
Hypothesis
Ref Expression
alexsub.1 |- X = U.J
Assertion
Ref Expression
alexsublem4 |- (J = (topGen` ( fi ` x)) -> (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b)))
Distinct variable groups:   a,b,c,d,x,J   X,a,b,c,d,x
Proof of Theorem alexsublem4
StepHypRef Expression
1 alexsub.1 . . . . . . . 8 |- X = U.J
21alexsublem2 15438 . . . . . . 7 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) -> E.u e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v)
3 elpwi 3039 . . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. ~P( fi ` x) -> u C_ ( fi ` x))
43sseld 2619 . . . . . . . . . . . . . . . . . . . . . 22 |- (u e. ~P( fi ` x) -> (w e. u -> w e. ( fi ` x)))
54ad2antrl 442 . . . . . . . . . . . . . . . . . . . . 21 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (w e. u -> w e. ( fi ` x)))
6 visset 2295 . . . . . . . . . . . . . . . . . . . . . 22 |- w e. _V
7 visset 2295 . . . . . . . . . . . . . . . . . . . . . 22 |- x e. _V
8 sppfi 10218 . . . . . . . . . . . . . . . . . . . . . 22 |- ((w e. _V /\ x e. _V) -> (w e. ( fi ` x) <-> E.t(t C_ x /\ t e. Fin /\ w = |^|t)))
96, 7, 8mp2an 761 . . . . . . . . . . . . . . . . . . . . 21 |- (w e. ( fi ` x) <-> E.t(t C_ x /\ t e. Fin /\ w = |^|t))
105, 9syl6ib 229 . . . . . . . . . . . . . . . . . . . 20 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (w e. u -> E.t(t C_ x /\ t e. Fin /\ w = |^|t)))
111alexsublem3 15439 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) -> E.s e. t A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)
123adantr 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) -> u C_ ( fi ` x))
1312ad2antlr 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) -> u C_ ( fi ` x))
1413ad2antrr 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> u C_ ( fi ` x))
15 abfi2 10216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x e. _V -> x C_ ( fi ` x))
167, 15ax-mp 7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- x C_ ( fi ` x)
1716a1i 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> x C_ ( fi ` x))
18 simpl1 879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) -> t C_ x)
1918ad2antlr 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> t C_ x)
20 simprl 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> s e. t)
2119, 20sseldd 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> s e. x)
2217, 21sseldd 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> s e. ( fi ` x))
2322snssd 3130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> {s} C_ ( fi ` x))
2414, 23jca 310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> (u C_ ( fi ` x) /\ {s} C_ ( fi ` x)))
25 unss 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((u C_ ( fi ` x) /\ {s} C_ ( fi ` x)) <-> (u u. {s}) C_ ( fi ` x))
2624, 25sylib 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> (u u. {s}) C_ ( fi ` x))
27 fvex 4689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( fi ` x) e. _V
2827elpw2 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((u u. {s}) e. ~P( fi ` x) <-> (u u. {s}) C_ ( fi ` x))
2926, 28sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> (u u. {s}) e. ~P( fi ` x))
30 simprl 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) -> a C_ u)
3130ad2antlr 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) -> a C_ u)
3231ad2antrr 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> a C_ u)
33 ssun1 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- u C_ (u u. {s})
3433a1i 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> u C_ (u u. {s}))
3532, 34sstrd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> a C_ (u u. {s}))
36 unieq 3185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (n = b -> U.n = U.b)
3736eqeq2d 1895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (n = b -> (X = U.n <-> X = U.b))
3837notbid 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (n = b -> (-. X = U.n <-> -. X = U.b))
3938cbvralv 2280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n <-> A.b e. (~P(u u. {s}) i^i Fin) -. X = U.b)
4039biimpi 168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n -> A.b e. (~P(u u. {s}) i^i Fin) -. X = U.b)
4140ad2antll 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> A.b e. (~P(u u. {s}) i^i Fin) -. X = U.b)
4229, 35, 41jca32 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> ((u u. {s}) e. ~P( fi ` x) /\ (a C_ (u u. {s}) /\ A.b e. (~P(u u. {s}) i^i Fin) -. X = U.b)))
43 sseq2 2639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (z = (u u. {s}) -> (a C_ z <-> a C_ (u u. {s})))
44 pweq 3036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (z = (u u. {s}) -> ~Pz = ~P(u u. {s}))
4544ineq1d 2795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (z = (u u. {s}) -> (~Pz i^i Fin) = (~P(u u. {s}) i^i Fin))
4645raleqdv 2269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (z = (u u. {s}) -> (A.b e. (~Pz i^i Fin) -. X = U.b <-> A.b e. (~P(u u. {s}) i^i Fin) -. X = U.b))
4743, 46anbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (z = (u u. {s}) -> ((a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b) <-> (a C_ (u u. {s}) /\ A.b e. (~P(u u. {s}) i^i Fin) -. X = U.b)))
4847elrab 2414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u u. {s}) e. {z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} <-> ((u u. {s}) e. ~P( fi ` x) /\ (a C_ (u u. {s}) /\ A.b e. (~P(u u. {s}) i^i Fin) -. X = U.b)))
4942, 48sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> (u u. {s}) e. {z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)})
50 elun1 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u u. {s}) e. {z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} -> (u u. {s}) e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}))
5149, 50syl 12 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> (u u. {s}) e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}))
52 sseq1 2637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (w = |^|t -> (w C_ s <-> |^|t C_ s))
53 intss1 3231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (s e. t -> |^|t C_ s)
5452, 53syl5cbir 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (s e. t -> (w = |^|t -> w C_ s))
5554impcom 378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((w = |^|t /\ s e. t) -> w C_ s)
56553ad2antl3 1040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (((t C_ x /\ t e. Fin /\ w = |^|t) /\ s e. t) -> w C_ s)
5756adantlr 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) /\ s e. t) -> w C_ s)
5857adantl 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((w e. u /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) /\ s e. t)) -> w C_ s)
5958adantrrr 439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((w e. u /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n))) -> w C_ s)
6059adantll 428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n))) -> w C_ s)
61 simprlr 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n))) -> y e. w)
6260, 61sseldd 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n))) -> y e. s)
63 simpl1 879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) -> t C_ x)
6463ad2antrl 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n))) -> t C_ x)
65 simprrl 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n))) -> s e. t)
6664, 65sseldd 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n))) -> s e. x)
67 elunii 3182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((y e. s /\ s e. (x i^i u)) -> y e. U.(x i^i u))
6867ex 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (y e. s -> (s e. (x i^i u) -> y e. U.(x i^i u)))
69 elin 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (s e. (x i^i u) <-> (s e. x /\ s e. u))
7068, 69syl5ibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (y e. s -> ((s e. x /\ s e. u) -> y e. U.(x i^i u)))
7170exp3a 405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (y e. s -> (s e. x -> (s e. u -> y e. U.(x i^i u))))
7262, 66, 71sylc 83 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n))) -> (s e. u -> y e. U.(x i^i u)))
7372con3d 111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n))) -> (-. y e. U.(x i^i u) -> -. s e. u))
7473expr 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w)) -> ((s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n) -> (-. y e. U.(x i^i u) -> -. s e. u)))
7574com23 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ y e. w)) -> (-. y e. U.(x i^i u) -> ((s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n) -> -. s e. u)))
7675exp32 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) -> ((t C_ x /\ t e. Fin /\ w = |^|t) -> (y e. w -> (-. y e. U.(x i^i u) -> ((s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n) -> -. s e. u)))))
7776imp55 15333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> -. s e. u)
78 visset 2295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- s e. _V
7978snid 3069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- s e. {s}
80 elun2 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (s e. {s} -> s e. (u u. {s}))
8179, 80ax-mp 7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- s e. (u u. {s})
8277, 81jctil 316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> (s e. (u u. {s}) /\ -. s e. u))
83 eleq1 1957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (v = s -> (v e. (u u. {s}) <-> s e. (u u. {s})))
84 elequ1 1496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (v = s -> (v e. u <-> s e. u))
8584notbid 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (v = s -> (-. v e. u <-> -. s e. u))
8683, 85anbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (v = s -> ((v e. (u u. {s}) /\ -. v e. u) <-> (s e. (u u. {s}) /\ -. s e. u)))
8778, 86cla4ev 2371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((s e. (u u. {s}) /\ -. s e. u) -> E.v(v e. (u u. {s}) /\ -. v e. u))
8882, 87syl 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> E.v(v e. (u u. {s}) /\ -. v e. u))
89 nss 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (-. (u u. {s}) C_ u <-> E.v(v e. (u u. {s}) /\ -. v e. u))
9088, 89sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> -. (u u. {s}) C_ u)
91 eqimss2 2667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (u = (u u. {s}) -> (u u. {s}) C_ u)
9291necon3bi 2045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (-. (u u. {s}) C_ u -> u =/= (u u. {s}))
9390, 92syl 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> u =/= (u u. {s}))
9493, 33jctil 316 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> (u C_ (u u. {s}) /\ u =/= (u u. {s})))
95 df-pss 2607 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (u C. (u u. {s}) <-> (u C_ (u u. {s}) /\ u =/= (u u. {s})))
9694, 95sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> u C. (u u. {s}))
97 psseq2 2698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (v = (u u. {s}) -> (u C. v <-> u C. (u u. {s})))
9897rcla4ev 2381 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((u u. {s}) e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) /\ u C. (u u. {s})) -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v)
9951, 96, 98syl11anc 524 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) /\ (s e. t /\ A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)) -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v)
10099exp32 408 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) -> (s e. t -> (A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v)))
101100r19.23adv 2215 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) -> (E.s e. t A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v))
10211, 101mpd 29 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v)
103102exp45 417 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) -> ((t C_ x /\ t e. Fin /\ w = |^|t) -> (y e. w -> (-. y e. U.(x i^i u) -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v))))
10410319.23adv 1584 . . . . . . . . . . . . . . . . . . . . 21 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) -> (E.t(t C_ x /\ t e. Fin /\ w = |^|t) -> (y e. w -> (-. y e. U.(x i^i u) -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v))))
105104ex 402 . . . . . . . . . . . . . . . . . . . 20 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (w e. u -> (E.t(t C_ x /\ t e. Fin /\ w = |^|t) -> (y e. w -> (-. y e. U.(x i^i u) -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v)))))
10610, 105mpdd 57 . . . . . . . . . . . . . . . . . . 19 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (w e. u -> (y e. w -> (-. y e. U.(x i^i u) -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v))))
107106r19.23adv 2215 . . . . . . . . . . . . . . . . . 18 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (E.w e. u y e. w -> (-. y e. U.(x i^i u) -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v)))
108 eluni2 3181 . . . . . . . . . . . . . . . . . 18 |- (y e. U.u <-> E.w e. u y e. w)
109107, 108syl5ib 223 . . . . . . . . . . . . . . . . 17 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (y e. U.u -> (-. y e. U.(x i^i u) -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v)))
110109r19.23adv 2215 . . . . . . . . . . . . . . . 16 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (E.y e. U.u -. y e. U.(x i^i u) -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v))
111 eqss 2631 . . . . . . . . . . . . . . . . . . . 20 |- (U.u = U.(x i^i u) <-> (U.u C_ U.(x i^i u) /\ U.(x i^i u) C_ U.u))
112111notbii 204 . . . . . . . . . . . . . . . . . . 19 |- (-. U.u = U.(x i^i u) <-> -. (U.u C_ U.(x i^i u) /\ U.(x i^i u) C_ U.u))
113 ianor 329 . . . . . . . . . . . . . . . . . . 19 |- (-. (U.u C_ U.(x i^i u) /\ U.(x i^i u) C_ U.u) <-> (-. U.u C_ U.(x i^i u) \/ -. U.(x i^i u) C_ U.u))
114 df-or 241 . . . . . . . . . . . . . . . . . . . 20 |- ((-. U.(x i^i u) C_ U.u \/ -. U.u C_ U.(x i^i u)) <-> (-. -. U.(x i^i u) C_ U.u -> -. U.u C_ U.(x i^i u)))
115 orcom 266 . . . . . . . . . . . . . . . . . . . 20 |- ((-. U.u C_ U.(x i^i u) \/ -. U.(x i^i u) C_ U.u) <-> (-. U.(x i^i u) C_ U.u \/ -. U.u C_ U.(x i^i u)))
116 notnot 178 . . . . . . . . . . . . . . . . . . . . 21 |- (U.(x i^i u) C_ U.u <-> -. -. U.(x i^i u) C_ U.u)
117116imbi1i 203 . . . . . . . . . . . . . . . . . . . 20 |- ((U.(x i^i u) C_ U.u -> -. U.u C_ U.(x i^i u)) <-> (-. -. U.(x i^i u) C_ U.u -> -. U.u C_ U.(x i^i u)))
118114, 115, 1173bitr4i 200 . . . . . . . . . . . . . . . . . . 19 |- ((-. U.u C_ U.(x i^i u) \/ -. U.(x i^i u) C_ U.u) <-> (U.(x i^i u) C_ U.u -> -. U.u C_ U.(x i^i u)))
119112, 113, 1183bitri 194 . . . . . . . . . . . . . . . . . 18 |- (-. U.u = U.(x i^i u) <-> (U.(x i^i u) C_ U.u -> -. U.u C_ U.(x i^i u)))
120 inss2 2813 . . . . . . . . . . . . . . . . . . . 20 |- (x i^i u) C_ u
121 uniss 3199 . . . . . . . . . . . . . . . . . . . 20 |- ((x i^i u) C_ u -> U.(x i^i u) C_ U.u)
122120, 121ax-mp 7 . . . . . . . . . . . . . . . . . . 19 |- U.(x i^i u) C_ U.u
123 id 73 . . . . . . . . . . . . . . . . . . 19 |- ((U.(x i^i u) C_ U.u -> -. U.u C_ U.(x i^i u)) -> (U.(x i^i u) C_ U.u -> -. U.u C_ U.(x i^i u)))
124122, 123mpi 55 . . . . . . . . . . . . . . . . . 18 |- ((U.(x i^i u) C_ U.u -> -. U.u C_ U.(x i^i u)) -> -. U.u C_ U.(x i^i u))
125119, 124sylbi 216 . . . . . . . . . . . . . . . . 17 |- (-. U.u = U.(x i^i u) -> -. U.u C_ U.(x i^i u))
126 nss 2670 . . . . . . . . . . . . . . . . . 18 |- (-. U.u C_ U.(x i^i u) <-> E.y(y e. U.u /\ -. y e. U.(x i^i u)))
127 df-rex 2110 . . . . . . . . . . . . . . . . . 18 |- (E.y e. U.u -. y e. U.(x i^i u) <-> E.y(y e. U.u /\ -. y e. U.(x i^i u)))
128126, 127bitr4i 193 . . . . . . . . . . . . . . . . 17 |- (-. U.u C_ U.(x i^i u) <-> E.y e. U.u -. y e. U.(x i^i u))
129125, 128sylib 215 . . . . . . . . . . . . . . . 16 |- (-. U.u = U.(x i^i u) -> E.y e. U.u -. y e. U.(x i^i u))
130110, 129syl5 20 . . . . . . . . . . . . . . 15 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (-. U.u = U.(x i^i u) -> E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v))
131 dfrex2 2116 . . . . . . . . . . . . . . 15 |- (E.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})u C. v <-> -. A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v)
132130, 131syl6ib 229 . . . . . . . . . . . . . 14 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (-. U.u = U.(x i^i u) -> -. A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v))
133132con4d 91 . . . . . . . . . . . . 13 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v -> U.u = U.(x i^i u)))
134 inss1 2812 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x i^i u) C_ x
1357elpw2 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x i^i u) e. ~Px <-> (x i^i u) C_ x)
136134, 135mpbir 207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x i^i u) e. ~Px
137 unieq 3185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (c = (x i^i u) -> U.c = U.(x i^i u))
138137eqeq2d 1895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (c = (x i^i u) -> (X = U.c <-> X = U.(x i^i u)))
139 pweq 3036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (c = (x i^i u) -> ~Pc = ~P(x i^i u))
140139ineq1d 2795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (c = (x i^i u) -> (~Pc i^i Fin) = (~P(x i^i u) i^i Fin))
141140rexeqdv 2270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (c = (x i^i u) -> (E.d e. (~Pc i^i Fin)X = U.d <-> E.d e. (~P(x i^i u) i^i Fin)X = U.d))
142138, 141imbi12d 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (c = (x i^i u) -> ((X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) <-> (X = U.(x i^i u) -> E.d e. (~P(x i^i u) i^i Fin)X = U.d)))
143142rcla4cv 2377 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> ((x i^i u) e. ~Px -> (X = U.(x i^i u) -> E.d e. (~P(x i^i u) i^i Fin)X = U.d)))
144136, 143mpi 55 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> (X = U.(x i^i u) -> E.d e. (~P(x i^i u) i^i Fin)X = U.d))
145 sstr 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((d C_ (x i^i u) /\ (x i^i u) C_ u) -> d C_ u)
146120, 145mpan2 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (d C_ (x i^i u) -> d C_ u)
147146anim1i 361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((d C_ (x i^i u) /\ d e. Fin) -> (d C_ u /\ d e. Fin))
148 elin 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (d e. (~P(x i^i u) i^i Fin) <-> (d e. ~P(x i^i u) /\ d e. Fin))
149 visset 2295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- d e. _V
150149elpw 3037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (d e. ~P(x i^i u) <-> d C_ (x i^i u))
151150anbi1i 539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((d e. ~P(x i^i u) /\ d e. Fin) <-> (d C_ (x i^i u) /\ d e. Fin))
152148, 151bitri 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (d e. (~P(x i^i u) i^i Fin) <-> (d C_ (x i^i u) /\ d e. Fin))
153 elin 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (d e. (~Pu i^i Fin) <-> (d e. ~Pu /\ d e. Fin))
154149elpw 3037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (d e. ~Pu <-> d C_ u)
155154anbi1i 539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((d e. ~Pu /\ d e. Fin) <-> (d C_ u /\ d e. Fin))
156153, 155bitri 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (d e. (~Pu i^i Fin) <-> (d C_ u /\ d e. Fin))
157147, 152, 1563imtr4i 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (d e. (~P(x i^i u) i^i Fin) -> d e. (~Pu i^i Fin))
158157anim1i 361 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((d e. (~P(x i^i u) i^i Fin) /\ X = U.d) -> (d e. (~Pu i^i Fin) /\ X = U.d))
159158reximi2 2197 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.d e. (~P(x i^i u) i^i Fin)X = U.d -> E.d e. (~Pu i^i Fin)X = U.d)
160144, 159syl6 25 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> (X = U.(x i^i u) -> E.d e. (~Pu i^i Fin)X = U.d))
161 unieq 3185 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (d = b -> U.d = U.b)
162161eqeq2d 1895 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (d = b -> (X = U.d <-> X = U.b))
163162cbvrexv 2281 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.d e. (~Pu i^i Fin)X = U.d <-> E.b e. (~Pu i^i Fin)X = U.b)
164160, 163syl6ib 229 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> (X = U.(x i^i u) -> E.b e. (~Pu i^i Fin)X = U.b))
165 dfrex2 2116 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (E.b e. (~Pu i^i Fin)X = U.b <-> -. A.b e. (~Pu i^i Fin) -. X = U.b)
166164, 165syl6ib 229 . . . . . . . . . . . . . . . . . . . . . . 23 |- (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> (X = U.(x i^i u) -> -. A.b e. (~Pu i^i Fin) -. X = U.b))
167166con2d 107 . . . . . . . . . . . . . . . . . . . . . 22 |- (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> (A.b e. (~Pu i^i Fin) -. X = U.b -> -. X = U.(x i^i u)))
168167a1d 15 . . . . . . . . . . . . . . . . . . . . 21 |- (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> (a C_ u -> (A.b e. (~Pu i^i Fin) -. X = U.b -> -. X = U.(x i^i u))))
1691683ad2ant2 898 . . . . . . . . . . . . . . . . . . . 20 |- ((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) -> (a C_ u -> (A.b e. (~Pu i^i Fin) -. X = U.b -> -. X = U.(x i^i u))))
170169adantr 425 . . . . . . . . . . . . . . . . . . 19 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ u e. ~P( fi ` x)) -> (a C_ u -> (A.b e. (~Pu i^i Fin) -. X = U.b -> -. X = U.(x i^i u))))
171170imp3a 388 . . . . . . . . . . . . . . . . . 18 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ u e. ~P( fi ` x)) -> ((a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b) -> -. X = U.(x i^i u)))
172171impr 422 . . . . . . . . . . . . . . . . 17 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> -. X = U.(x i^i u))
173172adantrr 431 . . . . . . . . . . . . . . . 16 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u))) -> -. X = U.(x i^i u))
174 sseq2 2639 . . . . . . . . . . . . . . . . . . . . 21 |- (U.u = U.(x i^i u) -> (X C_ U.u <-> X C_ U.(x i^i u)))
175174biimpd 170 . . . . . . . . . . . . . . . . . . . 20 |- (U.u = U.(x i^i u) -> (X C_ U.u -> X C_ U.(x i^i u)))
176175ad2antll 443 . . . . . . . . . . . . . . . . . . 19 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u))) -> (X C_ U.u -> X C_ U.(x i^i u)))
177176impr 422 . . . . . . . . . . . . . . . . . 18 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u)) /\ X C_ U.u)) -> X C_ U.(x i^i u))
178 uniss 3199 . . . . . . . . . . . . . . . . . . . . 21 |- ((x i^i u) C_ x -> U.(x i^i u) C_ U.x)
179134, 178ax-mp 7 . . . . . . . . . . . . . . . . . . . 20 |- U.(x i^i u) C_ U.x
180179a1i 8 . . . . . . . . . . . . . . . . . . 19 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u)) /\ X C_ U.u)) -> U.(x i^i u) C_ U.x)
181 unieq 3185 . . . . . . . . . . . . . . . . . . . . . . 23 |- (J = (topGen` ( fi ` x)) -> U.J = U.(topGen` ( fi ` x)))
182 fiuni 10219 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. _V -> U.x = U.( fi ` x))
1837, 182ax-mp 7 . . . . . . . . . . . . . . . . . . . . . . . 24 |- U.x = U.( fi ` x)
184 fibas 10221 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. _V -> ( fi ` x) e. Bases)
1857, 184ax-mp 7 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( fi ` x) e. Bases
186 unitg 8893 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (( fi ` x) e. Bases -> U.(topGen` ( fi ` x)) = U.( fi ` x))
187185, 186ax-mp 7 . . . . . . . . . . . . . . . . . . . . . . . 24 |- U.(topGen` ( fi ` x)) = U.( fi ` x)
188183, 187eqtr4i 1911 . . . . . . . . . . . . . . . . . . . . . . 23 |- U.x = U.(topGen` ( fi ` x))
189181, 188syl6reqr 1947 . . . . . . . . . . . . . . . . . . . . . 22 |- (J = (topGen` ( fi ` x)) -> U.x = U.J)
190189, 1syl6eqr 1946 . . . . . . . . . . . . . . . . . . . . 21 |- (J = (topGen` ( fi ` x)) -> U.x = X)
1911903ad2ant1 897 . . . . . . . . . . . . . . . . . . . 20 |- ((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) -> U.x = X)
192191adantr 425 . . . . . . . . . . . . . . . . . . 19 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u)) /\ X C_ U.u)) -> U.x = X)
193180, 192sseqtrd 2653 . . . . . . . . . . . . . . . . . 18 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u)) /\ X C_ U.u)) -> U.(x i^i u) C_ X)
194177, 193eqssd 2633 . . . . . . . . . . . . . . . . 17 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u)) /\ X C_ U.u)) -> X = U.(x i^i u))
195194expr 418 . . . . . . . . . . . . . . . 16 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u))) -> (X C_ U.u -> X = U.(x i^i u)))
196173, 195mtod 123 . . . . . . . . . . . . . . 15 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u))) -> -. X C_ U.u)
197 sseq1 2637 . . . . . . . . . . . . . . . 16 |- (X = U.a -> (X C_ U.u <-> U.a C_ U.u))
198 uniss 3199 . . . . . . . . . . . . . . . . . 18 |- (a C_ u -> U.a C_ U.u)
199198ad2antrl 442 . . . . . . . . . . . . . . . . 17 |- ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) -> U.a C_ U.u)
200199ad2antrl 442 . . . . . . . . . . . . . . . 16 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u))) -> U.a C_ U.u)
201197, 200syl5cbir 228 . . . . . . . . . . . . . . 15 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u))) -> (X = U.a -> X C_ U.u))
202196, 201mtod 123 . . . . . . . . . . . . . 14 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) /\ U.u = U.(x i^i u))) -> -. X = U.a)
203202expr 418 . . . . . . . . . . . . 13 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (U.u = U.(x i^i u) -> -. X = U.a))
204133, 203syld 30 . . . . . . . . . . . 12 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v -> -. X = U.a))
205204ex 402 . . . . . . . . . . 11 |- ((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) -> ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) -> (A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v -> -. X = U.a)))
206205adantr 425 . . . . . . . . . 10 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) -> ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) -> (A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v -> -. X = U.a)))
207 ssun1 2767 . . . . . . . . . . . . . . 15 |- {z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} C_ ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})
208207a1i 8 . . . . . . . . . . . . . 14 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) /\ u = (/)) -> {z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} C_ ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}))
209 sseq2 2639 . . . . . . . . . . . . . . . . 17 |- (z = a -> (a C_ z <-> a C_ a))
210 pweq 3036 . . . . . . . . . . . . . . . . . . 19 |- (z = a -> ~Pz = ~Pa)
211210ineq1d 2795 . . . . . . . . . . . . . . . . . 18 |- (z = a -> (~Pz i^i Fin) = (~Pa i^i Fin))
212211raleqdv 2269 . . . . . . . . . . . . . . . . 17 |- (z = a -> (A.b e. (~Pz i^i Fin) -. X = U.b <-> A.b e. (~Pa i^i Fin) -. X = U.b))
213209, 212anbi12d 690 . . . . . . . . . . . . . . . 16 |- (z = a -> ((a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b) <-> (a C_ a /\ A.b e. (~Pa i^i Fin) -. X = U.b)))
214213elrab 2414 . . . . . . . . . . . . . . 15 |- (a e. {z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} <-> (a e. ~P( fi ` x) /\ (a C_ a /\ A.b e. (~Pa i^i Fin) -. X = U.b)))
215 simpll3 917 . . . . . . . . . . . . . . 15 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) /\ u = (/)) -> a e. ~P( fi ` x))
216 simplr 449 . . . . . . . . . . . . . . . 16 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) /\ u = (/)) -> A.b e. (~Pa i^i Fin) -. X = U.b)
217 ssid 2634 . . . . . . . . . . . . . . . 16 |- a C_ a
218216, 217jctil 316 . . . . . . . . . . . . . . 15 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) /\ u = (/)) -> (a C_ a /\ A.b e. (~Pa i^i Fin) -. X = U.b))
219214, 215, 218sylanbrc 527 . . . . . . . . . . . . . 14 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) /\ u = (/)) -> a e. {z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)})
220208, 219sseldd 2620 . . . . . . . . . . . . 13 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) /\ u = (/)) -> a e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}))
221 psseq2 2698 . . . . . . . . . . . . . . 15 |- (v = a -> (u C. v <-> u C. a))
222221notbid 673 . . . . . . . . . . . . . 14 |- (v = a -> (-. u C. v <-> -. u C. a))
223222rcla4v 2376 . . . . . . . . . . . . 13 |- (a e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -> (A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v -> -. u C. a))
224220, 223syl 12 . . . . . . . . . . . 12 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) /\ u = (/)) -> (A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v -> -. u C. a))
225 psseq1 2697 . . . . . . . . . . . . . . . 16 |- (u = (/) -> (u C. a <-> (/) C. a))
226225notbid 673 . . . . . . . . . . . . . . 15 |- (u = (/) -> (-. u C. a <-> -. (/) C. a))
227226imbi1d 675 . . . . . . . . . . . . . 14 |- (u = (/) -> ((-. u C. a -> -. X = U.a) <-> (-. (/) C. a -> -. X = U.a)))
228 unieq 3185 . . . . . . . . . . . . . . . . . . 19 |- (a = (/) -> U.a = U.(/))
229228eqeq2d 1895 . . . . . . . . . . . . . . . . . 18 |- (a = (/) -> (X = U.a <-> X = U.(/)))
230229notbid 673 . . . . . . . . . . . . . . . . 17 |- (a = (/) -> (-. X = U.a <-> -. X = U.(/)))
231 elin 2786 . . . . . . . . . . . . . . . . . . 19 |- ((/) e. (~Pa i^i Fin) <-> ((/) e. ~Pa /\ (/) e. Fin))
232 0elpw 3473 . . . . . . . . . . . . . . . . . . 19 |- (/) e. ~Pa
233 emfin 10165 . . . . . . . . . . . . . . . . . . 19 |- (/) e. Fin
234231, 232, 233mpbir2an 800 . . . . . . . . . . . . . . . . . 18 |- (/) e. (~Pa i^i Fin)
235 unieq 3185 . . . . . . . . . . . . . . . . . . . . 21 |- (b = (/) -> U.b = U.(/))
236235eqeq2d 1895 . . . . . . . . . . . . . . . . . . . 20 |- (b = (/) -> (X = U.b <-> X = U.(/)))
237236notbid 673 . . . . . . . . . . . . . . . . . . 19 |- (b = (/) -> (-. X = U.b <-> -. X = U.(/)))
238237rcla4cv 2377 . . . . . . . . . . . . . . . . . 18 |- (A.b e. (~Pa i^i Fin) -. X = U.b -> ((/) e. (~Pa i^i Fin) -> -. X = U.(/)))
239234, 238mpi 55 . . . . . . . . . . . . . . . . 17 |- (A.b e. (~Pa i^i Fin) -. X = U.b -> -. X = U.(/))
240230, 239syl5cbir 228 . . . . . . . . . . . . . . . 16 |- (A.b e. (~Pa i^i Fin) -. X = U.b -> (a = (/) -> -. X = U.a))
241240adantl 424 . . . . . . . . . . . . . . 15 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) -> (a = (/) -> -. X = U.a))
242 0pss 2910 . . . . . . . . . . . . . . . . 17 |- ((/) C. a <-> a =/= (/))
243242notbii 204 . . . . . . . . . . . . . . . 16 |- (-. (/) C. a <-> -. a =/= (/))
244 nne 2021 . . . . . . . . . . . . . . . 16 |- (-. a =/= (/) <-> a = (/))
245243, 244bitri 190 . . . . . . . . . . . . . . 15 |- (-. (/) C. a <-> a = (/))
246241, 245syl5ib 223 . . . . . . . . . . . . . 14 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) -> (-. (/) C. a -> -. X = U.a))
247227, 246syl5cbir 228 . . . . . . . . . . . . 13 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) -> (u = (/) -> (-. u C. a -> -. X = U.a)))
248247imp 377 . . . . . . . . . . . 12 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) /\ u = (/)) -> (-. u C. a -> -. X = U.a))
249224, 248syld 30 . . . . . . . . . . 11 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) /\ u = (/)) -> (A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v -> -. X = U.a))
250249ex 402 . . . . . . . . . 10 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) -> (u = (/) -> (A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v -> -. X = U.a)))
251206, 250jaod 469 . . . . . . . . 9 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) -> (((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) \/ u = (/)) -> (A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v -> -. X = U.a)))
252 elun 2741 . . . . . . . . . 10 |- (u e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) <-> (u e. {z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} \/ u e. {(/)}))
253 sseq2 2639 . . . . . . . . . . . . 13 |- (z = u -> (a C_ z <-> a C_ u))
254 pweq 3036 . . . . . . . . . . . . . . 15 |- (z = u -> ~Pz = ~Pu)
255254ineq1d 2795 . . . . . . . . . . . . . 14 |- (z = u -> (~Pz i^i Fin) = (~Pu i^i Fin))
256255raleqdv 2269 . . . . . . . . . . . . 13 |- (z = u -> (A.b e. (~Pz i^i Fin) -. X = U.b <-> A.b e. (~Pu i^i Fin) -. X = U.b))
257253, 256anbi12d 690 . . . . . . . . . . . 12 |- (z = u -> ((a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b) <-> (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)))
258257elrab 2414 . . . . . . . . . . 11 |- (u e. {z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} <-> (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)))
259 elsn 3058 . . . . . . . . . . 11 |- (u e. {(/)} <-> u = (/))
260258, 259orbi12i 277 . . . . . . . . . 10 |- ((u e. {z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} \/ u e. {(/)}) <-> ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) \/ u = (/)))
261252, 260bitri 190 . . . . . . . . 9 |- (u e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) <-> ((u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b)) \/ u = (/)))
262251, 261syl5ib 223 . . . . . . . 8 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) -> (u e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -> (A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v -> -. X = U.a)))
263262r19.23adv 2215 . . . . . . 7 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) -> (E.u e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)})A.v e. ({z e. ~P( fi ` x) | (a C_ z /\ A.b e. (~Pz i^i Fin) -. X = U.b)} u. {(/)}) -. u C. v -> -. X = U.a))
2642, 263mpd 29 . . . . . 6 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ A.b e. (~Pa i^i Fin) -. X = U.b) -> -. X = U.a)
265264ex 402 . . . . 5 |- ((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) -> (A.b e. (~Pa i^i Fin) -. X = U.b -> -. X = U.a))
266 ralnex 2113 . . . . 5 |- (A.b e. (~Pa i^i Fin) -. X = U.b <-> -. E.b e. (~Pa i^i Fin)X = U.b)
267265, 266syl5ibr 224 . . . 4 |- ((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) -> (-. E.b e. (~Pa i^i Fin)X = U.b -> -. X = U.a))
268267con4d 91 . . 3 |- ((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) -> (X = U.a -> E.b e. (~Pa i^i Fin)X = U.b))
2692683exp 1066 . 2 |- (J = (topGen` ( fi ` x)) -> (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> (a e. ~P( fi ` x) -> (X = U.a -> E.b e. (~Pa i^i Fin)X = U.b))))
270269r19.21adv 2181 1 |- (J = (topGen` ( fi ` x)) -> (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b)))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593   C. wpss 2594  (/)c0 2875  ~Pcpw 3032  {csn 3044  U.cuni 3177  |^|cint 3214  ` cfv 3998  Fincfn 5426  Basesctb 8859  topGenctg 8860   fi cfi 10210
This theorem is referenced by:  alexsub 15441
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-ac 5906
This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-iso 4015  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-dom 5428  df-fin 5430  df-bases 8863  df-topgen 8864  df-fi 10211
Copyright terms: Public domain