Theorem fnejoin2 15531

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

Assertion

Ref	Expression
fnejoin2	|- ((X e. A /\ S C_ {y | X = U.y}) -> A.v((X = U.v /\ A.x e. S xFnev) -> if(S = (/), {X}, U.S)Fnev))

Distinct variable groups:   x,v,y,A   v,S,x,y   v,X,x,y

Proof of Theorem fnejoin2

Step	Hyp	Ref	Expression
1		iftrue 2989	. . . . . 6 |- (S = (/) -> if(S = (/), {X}, U.S) = {X})
2	1	breq1d 3348	. . . . 5 |- (S = (/) -> (if(S = (/), {X}, U.S)Fnev <-> {X}Fnev))
3		visset 2295	. . . . . . . 8 |- v e. _V
4		eqid 1884	. . . . . . . . 9 |- U.{X} = U.{X}
5		eqid 1884	. . . . . . . . 9 |- U.v = U.v
6	4, 5	isfne2 15481	. . . . . . . 8 |- (v e. _V -> ({X}Fnev <-> (U.{X} = U.v /\ A.y e. {X}A.x e. y E.z e. v (x e. z /\ z C_ y))))
7	3, 6	ax-mp 7	. . . . . . 7 |- ({X}Fnev <-> (U.{X} = U.v /\ A.y e. {X}A.x e. y E.z e. v (x e. z /\ z C_ y)))
8		unisng 3194	. . . . . . . . 9 |- (X e. A -> U.{X} = X)
9	8	adantr 425	. . . . . . . 8 |- ((X e. A /\ X = U.v) -> U.{X} = X)
10		simpr 350	. . . . . . . 8 |- ((X e. A /\ X = U.v) -> X = U.v)
11	9, 10	eqtrd 1925	. . . . . . 7 |- ((X e. A /\ X = U.v) -> U.{X} = U.v)
12		simpr 350	. . . . . . . . . . . . . . . 16 |- ((x e. z /\ z e. v) -> z e. v)
13		simpl 346	. . . . . . . . . . . . . . . 16 |- ((x e. z /\ z e. v) -> x e. z)
14		elssuni 3206	. . . . . . . . . . . . . . . . 17 |- (z e. v -> z C_ U.v)
15	14	adantl 424	. . . . . . . . . . . . . . . 16 |- ((x e. z /\ z e. v) -> z C_ U.v)
16	12, 13, 15	jca32 312	. . . . . . . . . . . . . . 15 |- ((x e. z /\ z e. v) -> (z e. v /\ (x e. z /\ z C_ U.v)))
17	16	eximi 1387	. . . . . . . . . . . . . 14 |- (E.z(x e. z /\ z e. v) -> E.z(z e. v /\ (x e. z /\ z C_ U.v)))
18		eluni 3180	. . . . . . . . . . . . . 14 |- (x e. U.v <-> E.z(x e. z /\ z e. v))
19		df-rex 2110	. . . . . . . . . . . . . 14 |- (E.z e. v (x e. z /\ z C_ U.v) <-> E.z(z e. v /\ (x e. z /\ z C_ U.v)))
20	17, 18, 19	3imtr4i 236	. . . . . . . . . . . . 13 |- (x e. U.v -> E.z e. v (x e. z /\ z C_ U.v))
21		eleq2 1958	. . . . . . . . . . . . . 14 |- (X = U.v -> (x e. X <-> x e. U.v))
22		sseq2 2639	. . . . . . . . . . . . . . . 16 |- (X = U.v -> (z C_ X <-> z C_ U.v))
23	22	anbi2d 678	. . . . . . . . . . . . . . 15 |- (X = U.v -> ((x e. z /\ z C_ X) <-> (x e. z /\ z C_ U.v)))
24	23	rexbidv 2124	. . . . . . . . . . . . . 14 |- (X = U.v -> (E.z e. v (x e. z /\ z C_ X) <-> E.z e. v (x e. z /\ z C_ U.v)))
25	21, 24	imbi12d 688	. . . . . . . . . . . . 13 |- (X = U.v -> ((x e. X -> E.z e. v (x e. z /\ z C_ X)) <-> (x e. U.v -> E.z e. v (x e. z /\ z C_ U.v))))
26	20, 25	mpbiri 211	. . . . . . . . . . . 12 |- (X = U.v -> (x e. X -> E.z e. v (x e. z /\ z C_ X)))
27	26	ad2antlr 441	. . . . . . . . . . 11 |- (((X e. A /\ X = U.v) /\ y = X) -> (x e. X -> E.z e. v (x e. z /\ z C_ X)))
28		eleq2 1958	. . . . . . . . . . . 12 |- (y = X -> (x e. y <-> x e. X))
29	28	adantl 424	. . . . . . . . . . 11 |- (((X e. A /\ X = U.v) /\ y = X) -> (x e. y <-> x e. X))
30		sseq2 2639	. . . . . . . . . . . . . 14 |- (y = X -> (z C_ y <-> z C_ X))
31	30	anbi2d 678	. . . . . . . . . . . . 13 |- (y = X -> ((x e. z /\ z C_ y) <-> (x e. z /\ z C_ X)))
32	31	rexbidv 2124	. . . . . . . . . . . 12 |- (y = X -> (E.z e. v (x e. z /\ z C_ y) <-> E.z e. v (x e. z /\ z C_ X)))
33	32	adantl 424	. . . . . . . . . . 11 |- (((X e. A /\ X = U.v) /\ y = X) -> (E.z e. v (x e. z /\ z C_ y) <-> E.z e. v (x e. z /\ z C_ X)))
34	27, 29, 33	3imtr4d 602	. . . . . . . . . 10 |- (((X e. A /\ X = U.v) /\ y = X) -> (x e. y -> E.z e. v (x e. z /\ z C_ y)))
35	34	expimpd 404	. . . . . . . . 9 |- ((X e. A /\ X = U.v) -> ((y = X /\ x e. y) -> E.z e. v (x e. z /\ z C_ y)))
36		elsni 3066	. . . . . . . . 9 |- (y e. {X} -> y = X)
37	35, 36	sylani 513	. . . . . . . 8 |- ((X e. A /\ X = U.v) -> ((y e. {X} /\ x e. y) -> E.z e. v (x e. z /\ z C_ y)))
38	37	r19.21aivv 2183	. . . . . . 7 |- ((X e. A /\ X = U.v) -> A.y e. {X}A.x e. y E.z e. v (x e. z /\ z C_ y))
39	7, 11, 38	sylanbrc 527	. . . . . 6 |- ((X e. A /\ X = U.v) -> {X}Fnev)
40	39	ad2ant2r 445	. . . . 5 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) -> {X}Fnev)
41	2, 40	syl5cbir 228	. . . 4 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) -> (S = (/) -> if(S = (/), {X}, U.S)Fnev))
42		eqid 1884	. . . . . . . . 9 |- U.U.S = U.U.S
43	42, 5	isfne2 15481	. . . . . . . 8 |- (v e. _V -> (U.SFnev <-> (U.U.S = U.v /\ A.z e. U.SA.w e. z E.t e. v (w e. t /\ t C_ z))))
44	3, 43	ax-mp 7	. . . . . . 7 |- (U.SFnev <-> (U.U.S = U.v /\ A.z e. U.SA.w e. z E.t e. v (w e. t /\ t C_ z)))
45		ssel 2615	. . . . . . . . . . . . . . . . . 18 |- (S C_ {y | X = U.y} -> (k e. S -> k e. {y | X = U.y}))
46		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . . 23 |- (t e. k -> t C_ U.k)
47	46	adantl 424	. . . . . . . . . . . . . . . . . . . . . 22 |- ((X = U.k /\ t e. k) -> t C_ U.k)
48		simpl 346	. . . . . . . . . . . . . . . . . . . . . 22 |- ((X = U.k /\ t e. k) -> X = U.k)
49	47, 48	sseqtr4d 2654	. . . . . . . . . . . . . . . . . . . . 21 |- ((X = U.k /\ t e. k) -> t C_ X)
50	49	ex 402	. . . . . . . . . . . . . . . . . . . 20 |- (X = U.k -> (t e. k -> t C_ X))
51	50	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (X e. A -> (X = U.k -> (t e. k -> t C_ X)))
52		visset 2295	. . . . . . . . . . . . . . . . . . . 20 |- k e. _V
53		unieq 3185	. . . . . . . . . . . . . . . . . . . . 21 |- (y = k -> U.y = U.k)
54	53	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . 20 |- (y = k -> (X = U.y <-> X = U.k))
55	52, 54	elab 2403	. . . . . . . . . . . . . . . . . . 19 |- (k e. {y | X = U.y} <-> X = U.k)
56	51, 55	syl5ib 223	. . . . . . . . . . . . . . . . . 18 |- (X e. A -> (k e. {y | X = U.y} -> (t e. k -> t C_ X)))
57	45, 56	syl9r 72	. . . . . . . . . . . . . . . . 17 |- (X e. A -> (S C_ {y | X = U.y} -> (k e. S -> (t e. k -> t C_ X))))
58	57	com34 40	. . . . . . . . . . . . . . . 16 |- (X e. A -> (S C_ {y | X = U.y} -> (t e. k -> (k e. S -> t C_ X))))
59	58	imp4b 392	. . . . . . . . . . . . . . 15 |- ((X e. A /\ S C_ {y | X = U.y}) -> ((t e. k /\ k e. S) -> t C_ X))
60	59	adantr 425	. . . . . . . . . . . . . 14 |- (((X e. A /\ S C_ {y | X = U.y}) /\ -. S = (/)) -> ((t e. k /\ k e. S) -> t C_ X))
61	60	19.23adv 1584	. . . . . . . . . . . . 13 |- (((X e. A /\ S C_ {y | X = U.y}) /\ -. S = (/)) -> (E.k(t e. k /\ k e. S) -> t C_ X))
62		eluni 3180	. . . . . . . . . . . . 13 |- (t e. U.S <-> E.k(t e. k /\ k e. S))
63	61, 62	syl5ib 223	. . . . . . . . . . . 12 |- (((X e. A /\ S C_ {y | X = U.y}) /\ -. S = (/)) -> (t e. U.S -> t C_ X))
64	63	r19.21aiv 2175	. . . . . . . . . . 11 |- (((X e. A /\ S C_ {y | X = U.y}) /\ -. S = (/)) -> A.t e. U.St C_ X)
65		unissb 3208	. . . . . . . . . . 11 |- (U.U.S C_ X <-> A.t e. U.St C_ X)
66	64, 65	sylibr 217	. . . . . . . . . 10 |- (((X e. A /\ S C_ {y | X = U.y}) /\ -. S = (/)) -> U.U.S C_ X)
67		ssel 2615	. . . . . . . . . . . . . . . . . 18 |- (S C_ {y | X = U.y} -> (s e. S -> s e. {y | X = U.y}))
68	67	com12 14	. . . . . . . . . . . . . . . . 17 |- (s e. S -> (S C_ {y | X = U.y} -> s e. {y | X = U.y}))
69		eleq2 1958	. . . . . . . . . . . . . . . . . . . . 21 |- (X = U.s -> (t e. X <-> t e. U.s))
70	69	biimpd 170	. . . . . . . . . . . . . . . . . . . 20 |- (X = U.s -> (t e. X -> t e. U.s))
71		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . 22 |- (s e. S -> s C_ U.S)
72		uniss 3199	. . . . . . . . . . . . . . . . . . . . . 22 |- (s C_ U.S -> U.s C_ U.U.S)
73	71, 72	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (s e. S -> U.s C_ U.U.S)
74	73	sseld 2619	. . . . . . . . . . . . . . . . . . . 20 |- (s e. S -> (t e. U.s -> t e. U.U.S))
75	70, 74	syl9r 72	. . . . . . . . . . . . . . . . . . 19 |- (s e. S -> (X = U.s -> (t e. X -> t e. U.U.S)))
76	75	a1dd 53	. . . . . . . . . . . . . . . . . 18 |- (s e. S -> (X = U.s -> (X e. A -> (t e. X -> t e. U.U.S))))
77		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- s e. _V
78		unieq 3185	. . . . . . . . . . . . . . . . . . . 20 |- (y = s -> U.y = U.s)
79	78	eqeq2d 1895	. . . . . . . . . . . . . . . . . . 19 |- (y = s -> (X = U.y <-> X = U.s))
80	77, 79	elab 2403	. . . . . . . . . . . . . . . . . 18 |- (s e. {y | X = U.y} <-> X = U.s)
81	76, 80	syl5ib 223	. . . . . . . . . . . . . . . . 17 |- (s e. S -> (s e. {y | X = U.y} -> (X e. A -> (t e. X -> t e. U.U.S))))
82	68, 81	syld 30	. . . . . . . . . . . . . . . 16 |- (s e. S -> (S C_ {y | X = U.y} -> (X e. A -> (t e. X -> t e. U.U.S))))
83	82	com13 37	. . . . . . . . . . . . . . 15 |- (X e. A -> (S C_ {y | X = U.y} -> (s e. S -> (t e. X -> t e. U.U.S))))
84	83	imp 377	. . . . . . . . . . . . . 14 |- ((X e. A /\ S C_ {y | X = U.y}) -> (s e. S -> (t e. X -> t e. U.U.S)))
85	84	19.23adv 1584	. . . . . . . . . . . . 13 |- ((X e. A /\ S C_ {y | X = U.y}) -> (E.s s e. S -> (t e. X -> t e. U.U.S)))
86	85	imp 377	. . . . . . . . . . . 12 |- (((X e. A /\ S C_ {y | X = U.y}) /\ E.s s e. S) -> (t e. X -> t e. U.U.S))
87		neq0 2885	. . . . . . . . . . . 12 |- (-. S = (/) <-> E.s s e. S)
88	86, 87	sylan2b 501	. . . . . . . . . . 11 |- (((X e. A /\ S C_ {y | X = U.y}) /\ -. S = (/)) -> (t e. X -> t e. U.U.S))
89	88	ssrdv 2622	. . . . . . . . . 10 |- (((X e. A /\ S C_ {y | X = U.y}) /\ -. S = (/)) -> X C_ U.U.S)
90	66, 89	eqssd 2633	. . . . . . . . 9 |- (((X e. A /\ S C_ {y | X = U.y}) /\ -. S = (/)) -> U.U.S = X)
91	90	adantlr 429	. . . . . . . 8 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) /\ -. S = (/)) -> U.U.S = X)
92		simplrl 454	. . . . . . . 8 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) /\ -. S = (/)) -> X = U.v)
93	91, 92	eqtrd 1925	. . . . . . 7 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) /\ -. S = (/)) -> U.U.S = U.v)
94		breq1 3341	. . . . . . . . . . . . . . . . 17 |- (x = s -> (xFnev <-> sFnev))
95	94	rcla4v 2376	. . . . . . . . . . . . . . . 16 |- (s e. S -> (A.x e. S xFnev -> sFnev))
96		fnessex 15484	. . . . . . . . . . . . . . . . . . . 20 |- (((v e. _V /\ sFnev /\ z e. s) /\ w e. z) -> E.t e. v (w e. t /\ t C_ z))
97	96	3exp1 1084	. . . . . . . . . . . . . . . . . . 19 |- (v e. _V -> (sFnev -> (z e. s -> (w e. z -> E.t e. v (w e. t /\ t C_ z)))))
98	3, 97	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- (sFnev -> (z e. s -> (w e. z -> E.t e. v (w e. t /\ t C_ z))))
99	98	a1dd 53	. . . . . . . . . . . . . . . . 17 |- (sFnev -> (z e. s -> ((X e. A /\ S C_ {y | X = U.y}) -> (w e. z -> E.t e. v (w e. t /\ t C_ z)))))
100	99	a1i24 15329	. . . . . . . . . . . . . . . 16 |- (sFnev -> (X = U.v -> (z e. s -> (-. S = (/) -> ((X e. A /\ S C_ {y | X = U.y}) -> (w e. z -> E.t e. v (w e. t /\ t C_ z)))))))
101	95, 100	syl6 25	. . . . . . . . . . . . . . 15 |- (s e. S -> (A.x e. S xFnev -> (X = U.v -> (z e. s -> (-. S = (/) -> ((X e. A /\ S C_ {y | X = U.y}) -> (w e. z -> E.t e. v (w e. t /\ t C_ z))))))))
102	101	com24 41	. . . . . . . . . . . . . 14 |- (s e. S -> (z e. s -> (X = U.v -> (A.x e. S xFnev -> (-. S = (/) -> ((X e. A /\ S C_ {y | X = U.y}) -> (w e. z -> E.t e. v (w e. t /\ t C_ z))))))))
103	102	impcom 378	. . . . . . . . . . . . 13 |- ((z e. s /\ s e. S) -> (X = U.v -> (A.x e. S xFnev -> (-. S = (/) -> ((X e. A /\ S C_ {y | X = U.y}) -> (w e. z -> E.t e. v (w e. t /\ t C_ z)))))))
104	103	com15 49	. . . . . . . . . . . 12 |- ((X e. A /\ S C_ {y | X = U.y}) -> (X = U.v -> (A.x e. S xFnev -> (-. S = (/) -> ((z e. s /\ s e. S) -> (w e. z -> E.t e. v (w e. t /\ t C_ z)))))))
105	104	imp42 396	. . . . . . . . . . 11 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) /\ -. S = (/)) -> ((z e. s /\ s e. S) -> (w e. z -> E.t e. v (w e. t /\ t C_ z))))
106	105	19.23adv 1584	. . . . . . . . . 10 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) /\ -. S = (/)) -> (E.s(z e. s /\ s e. S) -> (w e. z -> E.t e. v (w e. t /\ t C_ z))))
107	106	imp3a 388	. . . . . . . . 9 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) /\ -. S = (/)) -> ((E.s(z e. s /\ s e. S) /\ w e. z) -> E.t e. v (w e. t /\ t C_ z)))
108		eluni 3180	. . . . . . . . . 10 |- (z e. U.S <-> E.s(z e. s /\ s e. S))
109	108	biimpi 168	. . . . . . . . 9 |- (z e. U.S -> E.s(z e. s /\ s e. S))
110	107, 109	sylani 513	. . . . . . . 8 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) /\ -. S = (/)) -> ((z e. U.S /\ w e. z) -> E.t e. v (w e. t /\ t C_ z)))
111	110	r19.21aivv 2183	. . . . . . 7 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) /\ -. S = (/)) -> A.z e. U.SA.w e. z E.t e. v (w e. t /\ t C_ z))
112	44, 93, 111	sylanbrc 527	. . . . . 6 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) /\ -. S = (/)) -> U.SFnev)
113		iffalse 2991	. . . . . . . 8 |- (-. S = (/) -> if(S = (/), {X}, U.S) = U.S)
114	113	breq1d 3348	. . . . . . 7 |- (-. S = (/) -> (if(S = (/), {X}, U.S)Fnev <-> U.SFnev))
115	114	adantl 424	. . . . . 6 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) /\ -. S = (/)) -> (if(S = (/), {X}, U.S)Fnev <-> U.SFnev))
116	112, 115	mpbird 213	. . . . 5 |- ((((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) /\ -. S = (/)) -> if(S = (/), {X}, U.S)Fnev)
117	116	ex 402	. . . 4 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) -> (-. S = (/) -> if(S = (/), {X}, U.S)Fnev))
118	41, 117	pm2.61d 141	. . 3 |- (((X e. A /\ S C_ {y | X = U.y}) /\ (X = U.v /\ A.x e. S xFnev)) -> if(S = (/), {X}, U.S)Fnev)
119	118	ex 402	. 2 |- ((X e. A /\ S C_ {y | X = U.y}) -> ((X = U.v /\ A.x e. S xFnev) -> if(S = (/), {X}, U.S)Fnev))
120	119	19.21aiv 1664	1 |- ((X e. A /\ S C_ {y | X = U.y}) -> A.v((X = U.v /\ A.x e. S xFnev) -> if(S = (/), {X}, U.S)Fnev))

Syntax hints:  -. wn 2   -> 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  (/)c0 2875  ifcif 2982  {csn 3044  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-if 2983  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