Theorem fnemeet2 15529

Description: The meet of equivalence classes under the fineness relation-part two.

Assertion

Ref	Expression
fnemeet2	|- ((X e. A /\ S C_ {y | X = U.y}) -> A.v((X = U.v /\ A.x e. S vFnex) -> vFne{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))}))

Distinct variable groups:   u,t,v,w,x,y,z,A   t,S,u,v,w,x,y,z   t,X,u,v,w,x,y,z

Proof of Theorem fnemeet2

Step	Hyp	Ref	Expression
1		abssexg 3490	. . . . . 6 |- (X e. A -> {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} e. _V)
2		eqid 1884	. . . . . . 7 |- U.v = U.v
3		eqid 1884	. . . . . . 7 |- U.{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} = U.{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))}
4	2, 3	isfne2 15481	. . . . . 6 |- ({z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} e. _V -> (vFne{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} <-> (U.v = U.{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} /\ A.a e. v A.b e. a E.c e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} (b e. c /\ c C_ a))))
5	1, 4	syl 12	. . . . 5 |- (X e. A -> (vFne{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} <-> (U.v = U.{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} /\ A.a e. v A.b e. a E.c e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} (b e. c /\ c C_ a))))
6	5	ad2antrr 440	. . . 4 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> (vFne{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} <-> (U.v = U.{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} /\ A.a e. v A.b e. a E.c e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} (b e. c /\ c C_ a))))
7		simprl 450	. . . . 5 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> X = U.v)
8		ssel2 2616	. . . . . . . . . . . . . 14 |- ((S C_ {y | X = U.y} /\ t e. S) -> t e. {y | X = U.y})
9	8	adantll 428	. . . . . . . . . . . . 13 |- (((X e. A /\ S C_ {y | X = U.y}) /\ t e. S) -> t e. {y | X = U.y})
10	9	ad2ant2rl 447	. . . . . . . . . . . 12 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) /\ (w e. X /\ t e. S)) -> t e. {y | X = U.y})
11		eleq2 1958	. . . . . . . . . . . . . . . 16 |- (X = U.t -> (w e. X <-> w e. U.t))
12		simplrr 455	. . . . . . . . . . . . . . . . . . . 20 |- (((X = U.t /\ (w e. a /\ a e. t)) /\ (t e. S /\ ((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)))) -> a e. t)
13		simprl 450	. . . . . . . . . . . . . . . . . . . . . 22 |- ((X = U.t /\ (w e. a /\ a e. t)) -> w e. a)
14		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (a e. t -> a C_ U.t)
15	14	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((X = U.t /\ a e. t) -> a C_ U.t)
16		simpl 346	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((X = U.t /\ a e. t) -> X = U.t)
17	15, 16	sseqtr4d 2654	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((X = U.t /\ a e. t) -> a C_ X)
18	17	adantrl 430	. . . . . . . . . . . . . . . . . . . . . 22 |- ((X = U.t /\ (w e. a /\ a e. t)) -> a C_ X)
19	13, 18	jca 310	. . . . . . . . . . . . . . . . . . . . 21 |- ((X = U.t /\ (w e. a /\ a e. t)) -> (w e. a /\ a C_ X))
20	19	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- (((X = U.t /\ (w e. a /\ a e. t)) /\ (t e. S /\ ((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)))) -> (w e. a /\ a C_ X))
21		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = a -> (w e. u <-> w e. a))
22		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = a -> (u C_ X <-> a C_ X))
23	21, 22	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (u = a -> ((w e. u /\ u C_ X) <-> (w e. a /\ a C_ X)))
24	23	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . 20 |- ((a e. t /\ (w e. a /\ a C_ X)) -> E.u e. t (w e. u /\ u C_ X))
25	12, 20, 24	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 |- (((X = U.t /\ (w e. a /\ a e. t)) /\ (t e. S /\ ((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)))) -> E.u e. t (w e. u /\ u C_ X))
26	25	exp43 415	. . . . . . . . . . . . . . . . . 18 |- (X = U.t -> ((w e. a /\ a e. t) -> (t e. S -> (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> E.u e. t (w e. u /\ u C_ X)))))
27	26	19.23adv 1584	. . . . . . . . . . . . . . . . 17 |- (X = U.t -> (E.a(w e. a /\ a e. t) -> (t e. S -> (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> E.u e. t (w e. u /\ u C_ X)))))
28		eluni 3180	. . . . . . . . . . . . . . . . 17 |- (w e. U.t <-> E.a(w e. a /\ a e. t))
29	27, 28	syl5ib 223	. . . . . . . . . . . . . . . 16 |- (X = U.t -> (w e. U.t -> (t e. S -> (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> E.u e. t (w e. u /\ u C_ X)))))
30	11, 29	sylbid 220	. . . . . . . . . . . . . . 15 |- (X = U.t -> (w e. X -> (t e. S -> (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> E.u e. t (w e. u /\ u C_ X)))))
31	30	com14 42	. . . . . . . . . . . . . 14 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> (w e. X -> (t e. S -> (X = U.t -> E.u e. t (w e. u /\ u C_ X)))))
32	31	imp32 390	. . . . . . . . . . . . 13 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) /\ (w e. X /\ t e. S)) -> (X = U.t -> E.u e. t (w e. u /\ u C_ X)))
33		visset 2295	. . . . . . . . . . . . . 14 |- t e. _V
34		unieq 3185	. . . . . . . . . . . . . . 15 |- (y = t -> U.y = U.t)
35	34	eqeq2d 1895	. . . . . . . . . . . . . 14 |- (y = t -> (X = U.y <-> X = U.t))
36	33, 35	elab 2403	. . . . . . . . . . . . 13 |- (t e. {y | X = U.y} <-> X = U.t)
37	32, 36	syl5ib 223	. . . . . . . . . . . 12 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) /\ (w e. X /\ t e. S)) -> (t e. {y | X = U.y} -> E.u e. t (w e. u /\ u C_ X)))
38	10, 37	mpd 29	. . . . . . . . . . 11 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) /\ (w e. X /\ t e. S)) -> E.u e. t (w e. u /\ u C_ X))
39	38	ex 402	. . . . . . . . . 10 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> ((w e. X /\ t e. S) -> E.u e. t (w e. u /\ u C_ X)))
40	39	r19.21aivv 2183	. . . . . . . . 9 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> A.w e. X A.t e. S E.u e. t (w e. u /\ u C_ X))
41		ssid 2634	. . . . . . . . 9 |- X C_ X
42	40, 41	jctil 316	. . . . . . . 8 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> (X C_ X /\ A.w e. X A.t e. S E.u e. t (w e. u /\ u C_ X)))
43		sseq2 2639	. . . . . . . . . . . . . 14 |- (z = X -> (u C_ z <-> u C_ X))
44	43	anbi2d 678	. . . . . . . . . . . . 13 |- (z = X -> ((w e. u /\ u C_ z) <-> (w e. u /\ u C_ X)))
45	44	rexbidv 2124	. . . . . . . . . . . 12 |- (z = X -> (E.u e. t (w e. u /\ u C_ z) <-> E.u e. t (w e. u /\ u C_ X)))
46	45	ralbidv 2123	. . . . . . . . . . 11 |- (z = X -> (A.t e. S E.u e. t (w e. u /\ u C_ z) <-> A.t e. S E.u e. t (w e. u /\ u C_ X)))
47	46	raleqbi1dv 2271	. . . . . . . . . 10 |- (z = X -> (A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z) <-> A.w e. X A.t e. S E.u e. t (w e. u /\ u C_ X)))
48	47	elssabg 3462	. . . . . . . . 9 |- (X e. A -> (X e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} <-> (X C_ X /\ A.w e. X A.t e. S E.u e. t (w e. u /\ u C_ X))))
49	48	ad2antrr 440	. . . . . . . 8 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> (X e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} <-> (X C_ X /\ A.w e. X A.t e. S E.u e. t (w e. u /\ u C_ X))))
50	42, 49	mpbird 213	. . . . . . 7 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> X e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))})
51		elssuni 3206	. . . . . . 7 |- (X e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} -> X C_ U.{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))})
52	50, 51	syl 12	. . . . . 6 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> X C_ U.{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))})
53		simpl 346	. . . . . . . . . 10 |- ((a C_ X /\ A.w e. a A.t e. S E.u e. t (w e. u /\ u C_ a)) -> a C_ X)
54	53	a1i 8	. . . . . . . . 9 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> ((a C_ X /\ A.w e. a A.t e. S E.u e. t (w e. u /\ u C_ a)) -> a C_ X))
55		visset 2295	. . . . . . . . . 10 |- a e. _V
56		sseq1 2637	. . . . . . . . . . 11 |- (z = a -> (z C_ X <-> a C_ X))
57		sseq2 2639	. . . . . . . . . . . . . . 15 |- (z = a -> (u C_ z <-> u C_ a))
58	57	anbi2d 678	. . . . . . . . . . . . . 14 |- (z = a -> ((w e. u /\ u C_ z) <-> (w e. u /\ u C_ a)))
59	58	rexbidv 2124	. . . . . . . . . . . . 13 |- (z = a -> (E.u e. t (w e. u /\ u C_ z) <-> E.u e. t (w e. u /\ u C_ a)))
60	59	ralbidv 2123	. . . . . . . . . . . 12 |- (z = a -> (A.t e. S E.u e. t (w e. u /\ u C_ z) <-> A.t e. S E.u e. t (w e. u /\ u C_ a)))
61	60	raleqbi1dv 2271	. . . . . . . . . . 11 |- (z = a -> (A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z) <-> A.w e. a A.t e. S E.u e. t (w e. u /\ u C_ a)))
62	56, 61	anbi12d 690	. . . . . . . . . 10 |- (z = a -> ((z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z)) <-> (a C_ X /\ A.w e. a A.t e. S E.u e. t (w e. u /\ u C_ a))))
63	55, 62	elab 2403	. . . . . . . . 9 |- (a e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} <-> (a C_ X /\ A.w e. a A.t e. S E.u e. t (w e. u /\ u C_ a)))
64	54, 63	syl5ib 223	. . . . . . . 8 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> (a e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} -> a C_ X))
65	64	r19.21aiv 2175	. . . . . . 7 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> A.a e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))}a C_ X)
66		unissb 3208	. . . . . . 7 |- (U.{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} C_ X <-> A.a e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))}a C_ X)
67	65, 66	sylibr 217	. . . . . 6 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> U.{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} C_ X)
68	52, 67	eqssd 2633	. . . . 5 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> X = U.{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))})
69	7, 68	eqtr3d 1927	. . . 4 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> U.v = U.{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))})
70		elssuni 3206	. . . . . . . . . . . 12 |- (a e. v -> a C_ U.v)
71	70	adantl 424	. . . . . . . . . . 11 |- ((X = U.v /\ a e. v) -> a C_ U.v)
72		simpl 346	. . . . . . . . . . 11 |- ((X = U.v /\ a e. v) -> X = U.v)
73	71, 72	sseqtr4d 2654	. . . . . . . . . 10 |- ((X = U.v /\ a e. v) -> a C_ X)
74	73	adantlr 429	. . . . . . . . 9 |- (((X = U.v /\ A.x e. S vFnex) /\ a e. v) -> a C_ X)
75	74	ad2ant2lr 446	. . . . . . . 8 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) /\ (a e. v /\ b e. a)) -> a C_ X)
76		breq2 3342	. . . . . . . . . . . . . . . 16 |- (x = t -> (vFnex <-> vFnet))
77	76	rcla4v 2376	. . . . . . . . . . . . . . 15 |- (t e. S -> (A.x e. S vFnex -> vFnet))
78	77	adantl 424	. . . . . . . . . . . . . 14 |- ((w e. a /\ t e. S) -> (A.x e. S vFnex -> vFnet))
79		simplr 449	. . . . . . . . . . . . . . . . 17 |- (((w e. a /\ t e. S) /\ vFnet) -> t e. S)
80	79	ad2antrr 440	. . . . . . . . . . . . . . . 16 |- (((((w e. a /\ t e. S) /\ vFnet) /\ (X = U.v /\ (a e. v /\ b e. a))) /\ (X e. A /\ S C_ {y | X = U.y})) -> t e. S)
81		simpllr 453	. . . . . . . . . . . . . . . 16 |- (((((w e. a /\ t e. S) /\ vFnet) /\ (X = U.v /\ (a e. v /\ b e. a))) /\ (X e. A /\ S C_ {y | X = U.y})) -> vFnet)
82		simprl 450	. . . . . . . . . . . . . . . . 17 |- ((X = U.v /\ (a e. v /\ b e. a)) -> a e. v)
83	82	ad2antlr 441	. . . . . . . . . . . . . . . 16 |- (((((w e. a /\ t e. S) /\ vFnet) /\ (X = U.v /\ (a e. v /\ b e. a))) /\ (X e. A /\ S C_ {y | X = U.y})) -> a e. v)
84		simpll 448	. . . . . . . . . . . . . . . . 17 |- (((w e. a /\ t e. S) /\ vFnet) -> w e. a)
85	84	ad2antrr 440	. . . . . . . . . . . . . . . 16 |- (((((w e. a /\ t e. S) /\ vFnet) /\ (X = U.v /\ (a e. v /\ b e. a))) /\ (X e. A /\ S C_ {y | X = U.y})) -> w e. a)
86		fnessex 15484	. . . . . . . . . . . . . . . 16 |- (((t e. S /\ vFnet /\ a e. v) /\ w e. a) -> E.u e. t (w e. u /\ u C_ a))
87	80, 81, 83, 85, 86	syl31anc 1103	. . . . . . . . . . . . . . 15 |- (((((w e. a /\ t e. S) /\ vFnet) /\ (X = U.v /\ (a e. v /\ b e. a))) /\ (X e. A /\ S C_ {y | X = U.y})) -> E.u e. t (w e. u /\ u C_ a))
88	87	exp53 419	. . . . . . . . . . . . . 14 |- ((w e. a /\ t e. S) -> (vFnet -> (X = U.v -> ((a e. v /\ b e. a) -> ((X e. A /\ S C_ {y | X = U.y}) -> E.u e. t (w e. u /\ u C_ a))))))
89	78, 88	syld 30	. . . . . . . . . . . . 13 |- ((w e. a /\ t e. S) -> (A.x e. S vFnex -> (X = U.v -> ((a e. v /\ b e. a) -> ((X e. A /\ S C_ {y | X = U.y}) -> E.u e. t (w e. u /\ u C_ a))))))
90	89	com23 36	. . . . . . . . . . . 12 |- ((w e. a /\ t e. S) -> (X = U.v -> (A.x e. S vFnex -> ((a e. v /\ b e. a) -> ((X e. A /\ S C_ {y | X = U.y}) -> E.u e. t (w e. u /\ u C_ a))))))
91	90	imp3a 388	. . . . . . . . . . 11 |- ((w e. a /\ t e. S) -> ((X = U.v /\ A.x e. S vFnex) -> ((a e. v /\ b e. a) -> ((X e. A /\ S C_ {y | X = U.y}) -> E.u e. t (w e. u /\ u C_ a)))))
92	91	com14 42	. . . . . . . . . 10 |- ((X e. A /\ S C_ {y | X = U.y}) -> ((X = U.v /\ A.x e. S vFnex) -> ((a e. v /\ b e. a) -> ((w e. a /\ t e. S) -> E.u e. t (w e. u /\ u C_ a)))))
93	92	imp31 389	. . . . . . . . 9 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) /\ (a e. v /\ b e. a)) -> ((w e. a /\ t e. S) -> E.u e. t (w e. u /\ u C_ a)))
94	93	r19.21aivv 2183	. . . . . . . 8 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) /\ (a e. v /\ b e. a)) -> A.w e. a A.t e. S E.u e. t (w e. u /\ u C_ a))
95	63, 75, 94	sylanbrc 527	. . . . . . 7 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) /\ (a e. v /\ b e. a)) -> a e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))})
96		simprr 451	. . . . . . . 8 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) /\ (a e. v /\ b e. a)) -> b e. a)
97		ssid 2634	. . . . . . . 8 |- a C_ a
98	96, 97	jctir 317	. . . . . . 7 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) /\ (a e. v /\ b e. a)) -> (b e. a /\ a C_ a))
99		eleq2 1958	. . . . . . . . 9 |- (c = a -> (b e. c <-> b e. a))
100		sseq1 2637	. . . . . . . . 9 |- (c = a -> (c C_ a <-> a C_ a))
101	99, 100	anbi12d 690	. . . . . . . 8 |- (c = a -> ((b e. c /\ c C_ a) <-> (b e. a /\ a C_ a)))
102	101	rcla4ev 2381	. . . . . . 7 |- ((a e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} /\ (b e. a /\ a C_ a)) -> E.c e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} (b e. c /\ c C_ a))
103	95, 98, 102	syl11anc 524	. . . . . 6 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) /\ (a e. v /\ b e. a)) -> E.c e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} (b e. c /\ c C_ a))
104	103	ex 402	. . . . 5 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> ((a e. v /\ b e. a) -> E.c e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} (b e. c /\ c C_ a)))
105	104	r19.21aivv 2183	. . . 4 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> A.a e. v A.b e. a E.c e. {z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))} (b e. c /\ c C_ a))
106	6, 69, 105	mpbir2and 802	. . 3 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S vFnex)) -> vFne{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))})
107	106	ex 402	. 2 |- ((X e. A /\ S C_ {y | X = U.y}) -> ((X = U.v /\ A.x e. S vFnex) -> vFne{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))}))
108	107	19.21aiv 1664	1 |- ((X e. A /\ S C_ {y | X = U.y}) -> A.v((X = U.v /\ A.x e. S vFnex) -> vFne{z | (z C_ X /\ A.w e. z A.t e. S E.u e. t (w e. u /\ u C_ z))}))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  U.cuni 3177   class class class wbr 3338  Fnecfne 15457

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-nul 3445  ax-pow 3481  ax-pr 3524  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-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  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-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-xp 4000  df-rel 4001  df-fne 15463

Copyright terms: Public domain