Theorem filssufillem 15570

Description: Lemma for filssufil 15571.

Hypothesis

Ref	Expression
filssufil.1	|- X = U.F

Assertion

Ref	Expression
filssufillem	|- (k e. Fil -> A.x((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f)) -> U.x e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})))

Distinct variable groups:   f,g,h,k,x,F   f,X,g,h,k,x

Proof of Theorem filssufillem

Step	Hyp	Ref	Expression
1		uncom 2744	. . . . . . . . . 10 |- ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) = ({g e. Fil | (U.k = U.g /\ k C_ g)} u. {(/)})
2	1	sseq2i 2642	. . . . . . . . 9 |- (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) <-> x C_ ({g e. Fil | (U.k = U.g /\ k C_ g)} u. {(/)}))
3		disjssun 2932	. . . . . . . . . . 11 |- ((x i^i {g e. Fil | (U.k = U.g /\ k C_ g)}) = (/) -> (x C_ ({g e. Fil | (U.k = U.g /\ k C_ g)} u. {(/)}) <-> x C_ {(/)}))
4	3	biimpcd 172	. . . . . . . . . 10 |- (x C_ ({g e. Fil | (U.k = U.g /\ k C_ g)} u. {(/)}) -> ((x i^i {g e. Fil | (U.k = U.g /\ k C_ g)}) = (/) -> x C_ {(/)}))
5	4	necon3bd 2039	. . . . . . . . 9 |- (x C_ ({g e. Fil | (U.k = U.g /\ k C_ g)} u. {(/)}) -> (-. x C_ {(/)} -> (x i^i {g e. Fil | (U.k = U.g /\ k C_ g)}) =/= (/)))
6	2, 5	sylbi 216	. . . . . . . 8 |- (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (-. x C_ {(/)} -> (x i^i {g e. Fil | (U.k = U.g /\ k C_ g)}) =/= (/)))
7	6	ad2antrl 442	. . . . . . 7 |- ((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) -> (-. x C_ {(/)} -> (x i^i {g e. Fil | (U.k = U.g /\ k C_ g)}) =/= (/)))
8		df-3an 860	. . . . . . . . . . . . 13 |- ((U.k = U.U.x /\ U.x e. Fil /\ k C_ U.x) <-> ((U.k = U.U.x /\ U.x e. Fil) /\ k C_ U.x))
9		unieq 3185	. . . . . . . . . . . . . . . . . . . . . 22 |- (g = j -> U.g = U.j)
10	9	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . 21 |- (g = j -> (U.k = U.g <-> U.k = U.j))
11		sseq2 2639	. . . . . . . . . . . . . . . . . . . . 21 |- (g = j -> (k C_ g <-> k C_ j))
12	10, 11	anbi12d 690	. . . . . . . . . . . . . . . . . . . 20 |- (g = j -> ((U.k = U.g /\ k C_ g) <-> (U.k = U.j /\ k C_ j)))
13	12	elrab 2414	. . . . . . . . . . . . . . . . . . 19 |- (j e. {g e. Fil | (U.k = U.g /\ k C_ g)} <-> (j e. Fil /\ (U.k = U.j /\ k C_ j)))
14		simprr 451	. . . . . . . . . . . . . . . . . . 19 |- ((j e. Fil /\ (U.k = U.j /\ k C_ j)) -> k C_ j)
15	13, 14	sylbi 216	. . . . . . . . . . . . . . . . . 18 |- (j e. {g e. Fil | (U.k = U.g /\ k C_ g)} -> k C_ j)
16	15	ad2antll 443	. . . . . . . . . . . . . . . . 17 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> k C_ j)
17		elssuni 3206	. . . . . . . . . . . . . . . . . 18 |- (j e. x -> j C_ U.x)
18	17	ad2antrl 442	. . . . . . . . . . . . . . . . 17 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> j C_ U.x)
19	16, 18	sstrd 2627	. . . . . . . . . . . . . . . 16 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> k C_ U.x)
20		uniss 3199	. . . . . . . . . . . . . . . 16 |- (k C_ U.x -> U.k C_ U.U.x)
21	19, 20	syl 12	. . . . . . . . . . . . . . 15 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> U.k C_ U.U.x)
22		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (b e. x -> b e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})))
23		elun 2741	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (b e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) <-> (b e. {(/)} \/ b e. {g e. Fil | (U.k = U.g /\ k C_ g)}))
24		elsn 3058	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (b e. {(/)} <-> b = (/))
25		noel 2879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- -. a e. (/)
26		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (b = (/) -> (a e. b <-> a e. (/)))
27	25, 26	mtbiri 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (b = (/) -> -. a e. b)
28	27	pm2.21d 94	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (b = (/) -> (a e. b -> a C_ U.k))
29	24, 28	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (b e. {(/)} -> (a e. b -> a C_ U.k))
30		unieq 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (g = b -> U.g = U.b)
31	30	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (g = b -> (U.k = U.g <-> U.k = U.b))
32		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (g = b -> (k C_ g <-> k C_ b))
33	31, 32	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (g = b -> ((U.k = U.g /\ k C_ g) <-> (U.k = U.b /\ k C_ b)))
34	33	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (b e. {g e. Fil | (U.k = U.g /\ k C_ g)} <-> (b e. Fil /\ (U.k = U.b /\ k C_ b)))
35		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (U.k = U.b -> (a C_ U.k <-> a C_ U.b))
36		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (a e. b -> a C_ U.b)
37	35, 36	syl5bir 227	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (U.k = U.b -> (a e. b -> a C_ U.k))
38	37	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((b e. Fil /\ (U.k = U.b /\ k C_ b)) -> (a e. b -> a C_ U.k))
39	34, 38	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (b e. {g e. Fil | (U.k = U.g /\ k C_ g)} -> (a e. b -> a C_ U.k))
40	29, 39	jaoi 368	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((b e. {(/)} \/ b e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (a e. b -> a C_ U.k))
41	23, 40	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (b e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (a e. b -> a C_ U.k))
42	22, 41	syl6 25	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (b e. x -> (a e. b -> a C_ U.k)))
43	42	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f)) -> (b e. x -> (a e. b -> a C_ U.k)))
44	43	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . 21 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (b e. x -> (a e. b -> a C_ U.k)))
45	44	com23 36	. . . . . . . . . . . . . . . . . . . 20 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (a e. b -> (b e. x -> a C_ U.k)))
46	45	imp3a 388	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> ((a e. b /\ b e. x) -> a C_ U.k))
47	46	19.23adv 1584	. . . . . . . . . . . . . . . . . 18 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (E.b(a e. b /\ b e. x) -> a C_ U.k))
48		eluni 3180	. . . . . . . . . . . . . . . . . 18 |- (a e. U.x <-> E.b(a e. b /\ b e. x))
49	47, 48	syl5ib 223	. . . . . . . . . . . . . . . . 17 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (a e. U.x -> a C_ U.k))
50	49	r19.21aiv 2175	. . . . . . . . . . . . . . . 16 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> A.a e. U.xa C_ U.k)
51		unissb 3208	. . . . . . . . . . . . . . . 16 |- (U.U.x C_ U.k <-> A.a e. U.xa C_ U.k)
52	50, 51	sylibr 217	. . . . . . . . . . . . . . 15 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> U.U.x C_ U.k)
53	21, 52	eqssd 2633	. . . . . . . . . . . . . 14 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> U.k = U.U.x)
54		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- (U.k = U.U.x -> (U.k e. U.x <-> U.U.x e. U.x))
55		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (U.k = U.j -> (U.k e. j <-> U.j e. j))
56		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- U.j = U.j
57	56	filusb 10267	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (j e. Fil -> U.j e. j)
58	55, 57	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . . . 23 |- (j e. Fil -> (U.k = U.j -> U.k e. j))
59	58	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 |- ((j e. Fil /\ U.k = U.j) -> U.k e. j)
60	59	adantrr 431	. . . . . . . . . . . . . . . . . . . . 21 |- ((j e. Fil /\ (U.k = U.j /\ k C_ j)) -> U.k e. j)
61	13, 60	sylbi 216	. . . . . . . . . . . . . . . . . . . 20 |- (j e. {g e. Fil | (U.k = U.g /\ k C_ g)} -> U.k e. j)
62	61	ad2antll 443	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> U.k e. j)
63	18, 62	sseldd 2620	. . . . . . . . . . . . . . . . . 18 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> U.k e. U.x)
64	54, 63	syl5cbi 226	. . . . . . . . . . . . . . . . 17 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (U.k = U.U.x -> U.U.x e. U.x))
65		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (w e. x -> w e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})))
66		elun 2741	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) <-> (w e. {(/)} \/ w e. {g e. Fil | (U.k = U.g /\ k C_ g)}))
67		elsn 3058	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w e. {(/)} <-> w = (/))
68		noel 2879	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- -. (/) e. (/)
69		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = (/) -> ((/) e. w <-> (/) e. (/)))
70	68, 69	mtbiri 785	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = (/) -> -. (/) e. w)
71	67, 70	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w e. {(/)} -> -. (/) e. w)
72		unieq 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (g = w -> U.g = U.w)
73	72	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (g = w -> (U.k = U.g <-> U.k = U.w))
74		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (g = w -> (k C_ g <-> k C_ w))
75	73, 74	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (g = w -> ((U.k = U.g /\ k C_ g) <-> (U.k = U.w /\ k C_ w)))
76	75	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w e. {g e. Fil | (U.k = U.g /\ k C_ g)} <-> (w e. Fil /\ (U.k = U.w /\ k C_ w)))
77		filesn 10268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w e. Fil -> -. (/) e. w)
78	77	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. Fil /\ (U.k = U.w /\ k C_ w)) -> -. (/) e. w)
79	76, 78	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w e. {g e. Fil | (U.k = U.g /\ k C_ g)} -> -. (/) e. w)
80	71, 79	jaoi 368	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((w e. {(/)} \/ w e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> -. (/) e. w)
81	66, 80	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> -. (/) e. w)
82	65, 81	syl6 25	. . . . . . . . . . . . . . . . . . . . . 22 |- (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (w e. x -> -. (/) e. w))
83	82	adantr 425	. . . . . . . . . . . . . . . . . . . . 21 |- ((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f)) -> (w e. x -> -. (/) e. w))
84	83	ad2antlr 441	. . . . . . . . . . . . . . . . . . . 20 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (w e. x -> -. (/) e. w))
85	84	con2d 107	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> ((/) e. w -> -. w e. x))
86	85	19.21aiv 1664	. . . . . . . . . . . . . . . . . 18 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> A.w((/) e. w -> -. w e. x))
87		alnex 1380	. . . . . . . . . . . . . . . . . . 19 |- (A.w -. ((/) e. w /\ w e. x) <-> -. E.w((/) e. w /\ w e. x))
88		imnan 261	. . . . . . . . . . . . . . . . . . . 20 |- (((/) e. w -> -. w e. x) <-> -. ((/) e. w /\ w e. x))
89	88	albii 1346	. . . . . . . . . . . . . . . . . . 19 |- (A.w((/) e. w -> -. w e. x) <-> A.w -. ((/) e. w /\ w e. x))
90		eluni 3180	. . . . . . . . . . . . . . . . . . . 20 |- ((/) e. U.x <-> E.w((/) e. w /\ w e. x))
91	90	notbii 204	. . . . . . . . . . . . . . . . . . 19 |- (-. (/) e. U.x <-> -. E.w((/) e. w /\ w e. x))
92	87, 89, 91	3bitr4i 200	. . . . . . . . . . . . . . . . . 18 |- (A.w((/) e. w -> -. w e. x) <-> -. (/) e. U.x)
93	86, 92	sylib 215	. . . . . . . . . . . . . . . . 17 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> -. (/) e. U.x)
94	64, 93	jctild 662	. . . . . . . . . . . . . . . 16 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (U.k = U.U.x -> (-. (/) e. U.x /\ U.U.x e. U.x)))
95		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w e. x -> w C_ U.x)
96	95	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ w e. x) /\ ((a e. w /\ b C_ U.U.x) /\ a C_ b)) -> w C_ U.x)
97	65	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) -> (w e. x -> w e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})))
98	97	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> (w e. x -> w e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})))
99		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (w = (/) -> (a e. w <-> a e. (/)))
100	25, 99	mtbiri 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (w = (/) -> -. a e. w)
101	100	pm2.21d 94	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (w = (/) -> (a e. w -> b e. w))
102	101	adantrd 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (w = (/) -> ((a e. w /\ b C_ U.U.x) -> b e. w))
103	102	adantrd 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (w = (/) -> (((a e. w /\ b C_ U.U.x) /\ a C_ b) -> b e. w))
104	103	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> (w = (/) -> (((a e. w /\ b C_ U.U.x) /\ a C_ b) -> b e. w)))
105	104, 67	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> (w e. {(/)} -> (((a e. w /\ b C_ U.U.x) /\ a C_ b) -> b e. w)))
106		simprll 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ ((w e. Fil /\ (U.k = U.w /\ k C_ w)) /\ ((a e. w /\ b C_ U.U.x) /\ a C_ b))) -> w e. Fil)
107		simpll 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((a e. w /\ b C_ U.U.x) /\ a C_ b) -> a e. w)
108	107	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ ((w e. Fil /\ (U.k = U.w /\ k C_ w)) /\ ((a e. w /\ b C_ U.U.x) /\ a C_ b))) -> a e. w)
109		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((a e. w /\ b C_ U.U.x) /\ a C_ b) -> b C_ U.U.x)
110	109	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ ((w e. Fil /\ (U.k = U.w /\ k C_ w)) /\ ((a e. w /\ b C_ U.U.x) /\ a C_ b))) -> b C_ U.U.x)
111		eqtr2 1905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((U.k = U.U.x /\ U.k = U.w) -> U.U.x = U.w)
112	111	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((U.k = U.U.x /\ (U.k = U.w /\ k C_ w)) -> U.U.x = U.w)
113	112	ad2ant2l 444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ (w e. Fil /\ (U.k = U.w /\ k C_ w))) -> U.U.x = U.w)
114	113	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ ((w e. Fil /\ (U.k = U.w /\ k C_ w)) /\ ((a e. w /\ b C_ U.U.x) /\ a C_ b))) -> U.U.x = U.w)
115	110, 114	sseqtrd 2653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ ((w e. Fil /\ (U.k = U.w /\ k C_ w)) /\ ((a e. w /\ b C_ U.U.x) /\ a C_ b))) -> b C_ U.w)
116		simprrr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ ((w e. Fil /\ (U.k = U.w /\ k C_ w)) /\ ((a e. w /\ b C_ U.U.x) /\ a C_ b))) -> a C_ b)
117	108, 115, 116	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ ((w e. Fil /\ (U.k = U.w /\ k C_ w)) /\ ((a e. w /\ b C_ U.U.x) /\ a C_ b))) -> (a e. w /\ b C_ U.w /\ a C_ b))
118		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- U.w = U.w
119	118	fillsb 10270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (w e. Fil -> ((a e. w /\ b C_ U.w /\ a C_ b) -> b e. w))
120	106, 117, 119	sylc 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ ((w e. Fil /\ (U.k = U.w /\ k C_ w)) /\ ((a e. w /\ b C_ U.U.x) /\ a C_ b))) -> b e. w)
121	120	exp32 408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> ((w e. Fil /\ (U.k = U.w /\ k C_ w)) -> (((a e. w /\ b C_ U.U.x) /\ a C_ b) -> b e. w)))
122	121, 76	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> (w e. {g e. Fil | (U.k = U.g /\ k C_ g)} -> (((a e. w /\ b C_ U.U.x) /\ a C_ b) -> b e. w)))
123	105, 122	jaod 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> ((w e. {(/)} \/ w e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (((a e. w /\ b C_ U.U.x) /\ a C_ b) -> b e. w)))
124	123, 66	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> (w e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (((a e. w /\ b C_ U.U.x) /\ a C_ b) -> b e. w)))
125	98, 124	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> (w e. x -> (((a e. w /\ b C_ U.U.x) /\ a C_ b) -> b e. w)))
126	125	imp31 389	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ w e. x) /\ ((a e. w /\ b C_ U.U.x) /\ a C_ b)) -> b e. w)
127	96, 126	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) /\ w e. x) /\ ((a e. w /\ b C_ U.U.x) /\ a C_ b)) -> b e. U.x)
128	127	exp58 15342	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> (w e. x -> (a e. w -> (b C_ U.U.x -> (a C_ b -> b e. U.x)))))
129	128	com23 36	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> (a e. w -> (w e. x -> (b C_ U.U.x -> (a C_ b -> b e. U.x)))))
130	129	imp3a 388	. . . . . . . . . . . . . . . . . . . . 21 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> ((a e. w /\ w e. x) -> (b C_ U.U.x -> (a C_ b -> b e. U.x))))
131	130	19.23adv 1584	. . . . . . . . . . . . . . . . . . . 20 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> (E.w(a e. w /\ w e. x) -> (b C_ U.U.x -> (a C_ b -> b e. U.x))))
132		eluni 3180	. . . . . . . . . . . . . . . . . . . 20 |- (a e. U.x <-> E.w(a e. w /\ w e. x))
133	131, 132	syl5ib 223	. . . . . . . . . . . . . . . . . . 19 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> (a e. U.x -> (b C_ U.U.x -> (a C_ b -> b e. U.x))))
134	133	3impd 1082	. . . . . . . . . . . . . . . . . 18 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> ((a e. U.x /\ b C_ U.U.x /\ a C_ b) -> b e. U.x))
135	134	19.21aivv 1665	. . . . . . . . . . . . . . . . 17 |- ((((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) /\ U.k = U.U.x) -> A.aA.b((a e. U.x /\ b C_ U.U.x /\ a C_ b) -> b e. U.x))
136	135	ex 402	. . . . . . . . . . . . . . . 16 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (U.k = U.U.x -> A.aA.b((a e. U.x /\ b C_ U.U.x /\ a C_ b) -> b e. U.x)))
137		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f = y -> (f C_ h <-> y C_ h))
138		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f = y -> (h C_ f <-> h C_ y))
139	137, 138	orbi12d 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f = y -> ((f C_ h \/ h C_ f) <-> (y C_ h \/ h C_ y)))
140		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (h = z -> (y C_ h <-> y C_ z))
141		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (h = z -> (h C_ y <-> z C_ y))
142	140, 141	orbi12d 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (h = z -> ((y C_ h \/ h C_ y) <-> (y C_ z \/ z C_ y)))
143	139, 142	rcla42v 2384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. x /\ z e. x) -> (A.f e. x A.h e. x (f C_ h \/ h C_ f) -> (y C_ z \/ z C_ y)))
144		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y C_ z -> (a e. y -> a e. z))
145		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (z e. x -> z C_ U.x)
146	145	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((z e. x /\ ((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ b e. z) /\ a e. z)) /\ ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ k e. Fil)) -> z C_ U.x)
147		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (z e. x -> z e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})))
148		elun 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (z e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) <-> (z e. {(/)} \/ z e. {g e. Fil | (U.k = U.g /\ k C_ g)}))
149		elsn 3058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (z e. {(/)} <-> z = (/))
150		noel 2879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- -. b e. (/)
151		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (z = (/) -> (b e. z <-> b e. (/)))
152	150, 151	mtbiri 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (z = (/) -> -. b e. z)
153	152	pm2.21d 94	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (z = (/) -> (b e. z -> (a e. z -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. z)))))
154	149, 153	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (z e. {(/)} -> (b e. z -> (a e. z -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. z)))))
155		unieq 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (g = z -> U.g = U.z)
156	155	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (g = z -> (U.k = U.g <-> U.k = U.z))
157		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (g = z -> (k C_ g <-> k C_ z))
158	156, 157	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (g = z -> ((U.k = U.g /\ k C_ g) <-> (U.k = U.z /\ k C_ z)))
159	158	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (z e. {g e. Fil | (U.k = U.g /\ k C_ g)} <-> (z e. Fil /\ (U.k = U.z /\ k C_ z)))
160		filint 10269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((z e. Fil /\ a e. z /\ b e. z) -> (a i^i b) e. z)
161	160	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (z e. Fil -> (a e. z -> (b e. z -> (a i^i b) e. z)))
162	161	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (z e. Fil -> (b e. z -> (a e. z -> (a i^i b) e. z)))
163	162	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((z e. Fil /\ (U.k = U.z /\ k C_ z)) -> (b e. z -> (a e. z -> (a i^i b) e. z)))
164	163	a1i4 15327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((z e. Fil /\ (U.k = U.z /\ k C_ z)) -> (b e. z -> (a e. z -> (k e. Fil -> (a i^i b) e. z))))
165	164	a1i4 15327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((z e. Fil /\ (U.k = U.z /\ k C_ z)) -> (b e. z -> (a e. z -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. z)))))
166	159, 165	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (z e. {g e. Fil | (U.k = U.g /\ k C_ g)} -> (b e. z -> (a e. z -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. z)))))
167	154, 166	jaoi 368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((z e. {(/)} \/ z e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (b e. z -> (a e. z -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. z)))))
168	148, 167	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (z e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (b e. z -> (a e. z -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. z)))))
169	147, 168	syl6com 64	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (z e. x -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (b e. z -> (a e. z -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. z))))))
170	169	imp4c 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (z e. x -> (((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ b e. z) /\ a e. z) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. z))))
171	170	imp43 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((z e. x /\ ((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ b e. z) /\ a e. z)) /\ ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ k e. Fil)) -> (a i^i b) e. z)
172	146, 171	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((z e. x /\ ((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ b e. z) /\ a e. z)) /\ ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ k e. Fil)) -> (a i^i b) e. U.x)
173	172	exp43 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (z e. x -> (((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ b e. z) /\ a e. z) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x))))
174	173	exp4c 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (z e. x -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (b e. z -> (a e. z -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x))))))
175	174	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (z e. x -> (a e. z -> (b e. z -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x))))))
176	175	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((y e. x /\ z e. x) -> (a e. z -> (b e. z -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x))))))
177	144, 176	syl9r 72	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((y e. x /\ z e. x) -> (y C_ z -> (a e. y -> (b e. z -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x)))))))
178		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (z C_ y -> (b e. z -> b e. y))
179		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (y e. x -> y C_ U.x)
180	179	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((y e. x /\ ((b e. y /\ a e. y) /\ x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}))) -> y C_ U.x)
181		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (y e. x -> y e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})))
182		elun 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (y e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) <-> (y e. {(/)} \/ y e. {g e. Fil | (U.k = U.g /\ k C_ g)}))
183		elsn 3058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (y e. {(/)} <-> y = (/))
184		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (y = (/) -> (b e. y <-> b e. (/)))
185	150, 184	mtbiri 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (y = (/) -> -. b e. y)
186	185	pm2.21d 94	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (y = (/) -> (b e. y -> (a i^i b) e. y))
187	186	adantrd 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (y = (/) -> ((b e. y /\ a e. y) -> (a i^i b) e. y))
188	183, 187	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (y e. {(/)} -> ((b e. y /\ a e. y) -> (a i^i b) e. y))
189		unieq 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (g = y -> U.g = U.y)
190	189	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (g = y -> (U.k = U.g <-> U.k = U.y))
191		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (g = y -> (k C_ g <-> k C_ y))
192	190, 191	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (g = y -> ((U.k = U.g /\ k C_ g) <-> (U.k = U.y /\ k C_ y)))
193	192	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (y e. {g e. Fil | (U.k = U.g /\ k C_ g)} <-> (y e. Fil /\ (U.k = U.y /\ k C_ y)))
194		filint 10269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((y e. Fil /\ a e. y /\ b e. y) -> (a i^i b) e. y)
195	194	3expib 1070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (y e. Fil -> ((a e. y /\ b e. y) -> (a i^i b) e. y))
196	195	ancomsd 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (y e. Fil -> ((b e. y /\ a e. y) -> (a i^i b) e. y))
197	196	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((y e. Fil /\ (U.k = U.y /\ k C_ y)) -> ((b e. y /\ a e. y) -> (a i^i b) e. y))
198	193, 197	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (y e. {g e. Fil | (U.k = U.g /\ k C_ g)} -> ((b e. y /\ a e. y) -> (a i^i b) e. y))
199	188, 198	jaoi 368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((y e. {(/)} \/ y e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((b e. y /\ a e. y) -> (a i^i b) e. y))
200	182, 199	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (y e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((b e. y /\ a e. y) -> (a i^i b) e. y))
201	181, 200	syl6com 64	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (y e. x -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((b e. y /\ a e. y) -> (a i^i b) e. y)))
202	201	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (y e. x -> ((b e. y /\ a e. y) -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (a i^i b) e. y)))
203	202	imp32 390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((y e. x /\ ((b e. y /\ a e. y) /\ x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}))) -> (a i^i b) e. y)
204	180, 203	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((y e. x /\ ((b e. y /\ a e. y) /\ x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}))) -> (a i^i b) e. U.x)
205	204	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (y e. x -> (((b e. y /\ a e. y) /\ x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (a i^i b) e. U.x))
206	205	a1i34 15330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (y e. x -> (((b e. y /\ a e. y) /\ x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x))))
207	206	exp4c 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (y e. x -> (b e. y -> (a e. y -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x))))))
208	207	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((y e. x /\ z e. x) -> (b e. y -> (a e. y -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x))))))
209	178, 208	syl9r 72	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((y e. x /\ z e. x) -> (z C_ y -> (b e. z -> (a e. y -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x)))))))
210	209	com34 40	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((y e. x /\ z e. x) -> (z C_ y -> (a e. y -> (b e. z -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x)))))))
211	177, 210	jaod 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. x /\ z e. x) -> ((y C_ z \/ z C_ y) -> (a e. y -> (b e. z -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x)))))))
212	143, 211	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y e. x /\ z e. x) -> (A.f e. x A.h e. x (f C_ h \/ h C_ f) -> (a e. y -> (b e. z -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x)))))))
213	212	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y e. x /\ z e. x) -> (b e. z -> (a e. y -> (A.f e. x A.h e. x (f C_ h \/ h C_ f) -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x)))))))
214	213	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. x -> (z e. x -> (b e. z -> (a e. y -> (A.f e. x A.h e. x (f C_ h \/ h C_ f) -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x))))))))
215	214	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. x -> (a e. y -> (b e. z -> (z e. x -> (A.f e. x A.h e. x (f C_ h \/ h C_ f) -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x))))))))
216	215	com12 14	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (a e. y -> (y e. x -> (b e. z -> (z e. x -> (A.f e. x A.h e. x (f C_ h \/ h C_ f) -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x))))))))
217	216	imp43 397	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((a e. y /\ y e. x) /\ (b e. z /\ z e. x)) -> (A.f e. x A.h e. x (f C_ h \/ h C_ f) -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (k e. Fil -> (a i^i b) e. U.x)))))
218	217	com15 49	. . . . . . . . . . . . . . . . . . . . . 22 |- (k e. Fil -> (A.f e. x A.h e. x (f C_ h \/ h C_ f) -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (((a e. y /\ y e. x) /\ (b e. z /\ z e. x)) -> (a i^i b) e. U.x)))))
219	218	com23 36	. . . . . . . . . . . . . . . . . . . . 21 |- (k e. Fil -> (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (A.f e. x A.h e. x (f C_ h \/ h C_ f) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (((a e. y /\ y e. x) /\ (b e. z /\ z e. x)) -> (a i^i b) e. U.x)))))
220	219	imp42 396	. . . . . . . . . . . . . . . . . . . 20 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (((a e. y /\ y e. x) /\ (b e. z /\ z e. x)) -> (a i^i b) e. U.x))
221	220	19.23advv 1676	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (E.yE.z((a e. y /\ y e. x) /\ (b e. z /\ z e. x)) -> (a i^i b) e. U.x))
222		eluni 3180	. . . . . . . . . . . . . . . . . . . . 21 |- (a e. U.x <-> E.y(a e. y /\ y e. x))
223		eluni 3180	. . . . . . . . . . . . . . . . . . . . 21 |- (b e. U.x <-> E.z(b e. z /\ z e. x))
224	222, 223	anbi12i 540	. . . . . . . . . . . . . . . . . . . 20 |- ((a e. U.x /\ b e. U.x) <-> (E.y(a e. y /\ y e. x) /\ E.z(b e. z /\ z e. x)))
225		eeanv 1707	. . . . . . . . . . . . . . . . . . . 20 |- (E.yE.z((a e. y /\ y e. x) /\ (b e. z /\ z e. x)) <-> (E.y(a e. y /\ y e. x) /\ E.z(b e. z /\ z e. x)))
226	224, 225	bitr4i 193	. . . . . . . . . . . . . . . . . . 19 |- ((a e. U.x /\ b e. U.x) <-> E.yE.z((a e. y /\ y e. x) /\ (b e. z /\ z e. x)))
227	221, 226	syl5ib 223	. . . . . . . . . . . . . . . . . 18 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> ((a e. U.x /\ b e. U.x) -> (a i^i b) e. U.x))
228	227	r19.21aivv 2183	. . . . . . . . . . . . . . . . 17 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> A.a e. U.xA.b e. U.x(a i^i b) e. U.x)
229	228	a1d 15	. . . . . . . . . . . . . . . 16 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (U.k = U.U.x -> A.a e. U.xA.b e. U.x(a i^i b) e. U.x))
230	94, 136, 229	3jcad 1051	. . . . . . . . . . . . . . 15 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (U.k = U.U.x -> ((-. (/) e. U.x /\ U.U.x e. U.x) /\ A.aA.b((a e. U.x /\ b C_ U.U.x /\ a C_ b) -> b e. U.x) /\ A.a e. U.xA.b e. U.x(a i^i b) e. U.x)))
231		visset 2295	. . . . . . . . . . . . . . . . 17 |- x e. _V
232	231	uniex 3794	. . . . . . . . . . . . . . . 16 |- U.x e. _V
233		eqid 1884	. . . . . . . . . . . . . . . . 17 |- U.U.x = U.U.x
234	233	isfil 10266	. . . . . . . . . . . . . . . 16 |- (U.x e. _V -> (U.x e. Fil <-> ((-. (/) e. U.x /\ U.U.x e. U.x) /\ A.aA.b((a e. U.x /\ b C_ U.U.x /\ a C_ b) -> b e. U.x) /\ A.a e. U.xA.b e. U.x(a i^i b) e. U.x)))
235	232, 234	ax-mp 7	. . . . . . . . . . . . . . 15 |- (U.x e. Fil <-> ((-. (/) e. U.x /\ U.U.x e. U.x) /\ A.aA.b((a e. U.x /\ b C_ U.U.x /\ a C_ b) -> b e. U.x) /\ A.a e. U.xA.b e. U.x(a i^i b) e. U.x))
236	230, 235	syl6ibr 230	. . . . . . . . . . . . . 14 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (U.k = U.U.x -> U.x e. Fil))
237	53, 236	jcai 313	. . . . . . . . . . . . 13 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (U.k = U.U.x /\ U.x e. Fil))
238	8, 237, 19	sylanbrc 527	. . . . . . . . . . . 12 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (U.k = U.U.x /\ U.x e. Fil /\ k C_ U.x))
239	238	3com12d 15347	. . . . . . . . . . 11 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (U.x e. Fil /\ U.k = U.U.x /\ k C_ U.x))
240		3anass 862	. . . . . . . . . . 11 |- ((U.x e. Fil /\ U.k = U.U.x /\ k C_ U.x) <-> (U.x e. Fil /\ (U.k = U.U.x /\ k C_ U.x)))
241	239, 240	sylib 215	. . . . . . . . . 10 |- (((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) /\ (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> (U.x e. Fil /\ (U.k = U.U.x /\ k C_ U.x)))
242	241	ex 402	. . . . . . . . 9 |- ((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) -> ((j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (U.x e. Fil /\ (U.k = U.U.x /\ k C_ U.x))))
243	242	19.23adv 1584	. . . . . . . 8 |- ((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) -> (E.j(j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}) -> (U.x e. Fil /\ (U.k = U.U.x /\ k C_ U.x))))
244		n0 2884	. . . . . . . . 9 |- ((x i^i {g e. Fil | (U.k = U.g /\ k C_ g)}) =/= (/) <-> E.j j e. (x i^i {g e. Fil | (U.k = U.g /\ k C_ g)}))
245		elin 2786	. . . . . . . . . 10 |- (j e. (x i^i {g e. Fil | (U.k = U.g /\ k C_ g)}) <-> (j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}))
246	245	exbii 1398	. . . . . . . . 9 |- (E.j j e. (x i^i {g e. Fil | (U.k = U.g /\ k C_ g)}) <-> E.j(j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}))
247	244, 246	bitri 190	. . . . . . . 8 |- ((x i^i {g e. Fil | (U.k = U.g /\ k C_ g)}) =/= (/) <-> E.j(j e. x /\ j e. {g e. Fil | (U.k = U.g /\ k C_ g)}))
248	243, 247	syl5ib 223	. . . . . . 7 |- ((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) -> ((x i^i {g e. Fil | (U.k = U.g /\ k C_ g)}) =/= (/) -> (U.x e. Fil /\ (U.k = U.U.x /\ k C_ U.x))))
249	7, 248	syld 30	. . . . . 6 |- ((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) -> (-. x C_ {(/)} -> (U.x e. Fil /\ (U.k = U.U.x /\ k C_ U.x))))
250		uni0b 3203	. . . . . . 7 |- (U.x = (/) <-> x C_ {(/)})
251	250	notbii 204	. . . . . 6 |- (-. U.x = (/) <-> -. x C_ {(/)})
252	249, 251	syl5ib 223	. . . . 5 |- ((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) -> (-. U.x = (/) -> (U.x e. Fil /\ (U.k = U.U.x /\ k C_ U.x))))
253	252	orrd 250	. . . 4 |- ((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) -> (U.x = (/) \/ (U.x e. Fil /\ (U.k = U.U.x /\ k C_ U.x))))
254		elun 2741	. . . . 5 |- (U.x e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) <-> (U.x e. {(/)} \/ U.x e. {g e. Fil | (U.k = U.g /\ k C_ g)}))
255	232	elsnc 3065	. . . . . 6 |- (U.x e. {(/)} <-> U.x = (/))
256		unieq 3185	. . . . . . . . 9 |- (g = U.x -> U.g = U.U.x)
257	256	eqeq2d 1895	. . . . . . . 8 |- (g = U.x -> (U.k = U.g <-> U.k = U.U.x))
258		sseq2 2639	. . . . . . . 8 |- (g = U.x -> (k C_ g <-> k C_ U.x))
259	257, 258	anbi12d 690	. . . . . . 7 |- (g = U.x -> ((U.k = U.g /\ k C_ g) <-> (U.k = U.U.x /\ k C_ U.x)))
260	259	elrab 2414	. . . . . 6 |- (U.x e. {g e. Fil | (U.k = U.g /\ k C_ g)} <-> (U.x e. Fil /\ (U.k = U.U.x /\ k C_ U.x)))
261	255, 260	orbi12i 277	. . . . 5 |- ((U.x e. {(/)} \/ U.x e. {g e. Fil | (U.k = U.g /\ k C_ g)}) <-> (U.x = (/) \/ (U.x e. Fil /\ (U.k = U.U.x /\ k C_ U.x))))
262	254, 261	bitr2i 191	. . . 4 |- ((U.x = (/) \/ (U.x e. Fil /\ (U.k = U.U.x /\ k C_ U.x))) <-> U.x e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}))
263	253, 262	sylib 215	. . 3 |- ((k e. Fil /\ (x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f))) -> U.x e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}))
264	263	ex 402	. 2 |- (k e. Fil -> ((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f)) -> U.x e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})))
265	264	19.21aiv 1664	1 |- (k e. Fil -> A.x((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f)) -> U.x e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  {crab 2108  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177  Filcfil 10264

This theorem is referenced by:  filssufil 15571

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-sep 3438  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-uni 3178  df-fil 10265

Copyright terms: Public domain