Theorem cncnplem4 7777

Description: Lemma for cncnp2 7779.

Hypothesis

Ref	Expression
cncnplem4.1	|- X = U.J

Assertion

Ref	Expression
cncnplem4	|- (J e. Top -> ((F:X-->Y /\ A.x e. X ((F` x) e. y -> E.z e. J (x e. z /\ (F"z) (_ y))) -> (`'F"y) e. J))

Distinct variable groups:   x,J,z   x,F,z   x,X,z   x,Y,z   x,y,z

Proof of Theorem cncnplem4

Step	Hyp	Ref	Expression
1		fdm 3631	. . . . . . . . . . . . . . 15 |- (F:X-->Y -> dom F = X)
2		cncnplem4.1	. . . . . . . . . . . . . . 15 |- X = U.J
3	1, 2	syl6eq 1523	. . . . . . . . . . . . . 14 |- (F:X-->Y -> dom F = U.J)
4	3	sseq2d 2089	. . . . . . . . . . . . 13 |- (F:X-->Y -> (z (_ dom F <-> z (_ U.J))
5		elssuni 2526	. . . . . . . . . . . . 13 |- (z e. J -> z (_ U.J)
6	4, 5	syl5bir 210	. . . . . . . . . . . 12 |- (F:X-->Y -> (z e. J -> z (_ dom F))
7		funimass3 3806	. . . . . . . . . . . . . 14 |- ((Fun F /\ z (_ dom F) -> ((F"z) (_ y <-> z (_ (`'F"y)))
8		ffun 3629	. . . . . . . . . . . . . 14 |- (F:X-->Y -> Fun F)
9	7, 8	sylan 448	. . . . . . . . . . . . 13 |- ((F:X-->Y /\ z (_ dom F) -> ((F"z) (_ y <-> z (_ (`'F"y)))
10	9	ex 373	. . . . . . . . . . . 12 |- (F:X-->Y -> (z (_ dom F -> ((F"z) (_ y <-> z (_ (`'F"y))))
11	6, 10	syld 27	. . . . . . . . . . 11 |- (F:X-->Y -> (z e. J -> ((F"z) (_ y <-> z (_ (`'F"y))))
12	11	imp 350	. . . . . . . . . 10 |- ((F:X-->Y /\ z e. J) -> ((F"z) (_ y <-> z (_ (`'F"y)))
13	12	anbi2d 616	. . . . . . . . 9 |- ((F:X-->Y /\ z e. J) -> ((x e. z /\ (F"z) (_ y) <-> (x e. z /\ z (_ (`'F"y))))
14	13	rabbidv 1806	. . . . . . . 8 |- (F:X-->Y -> {z e. J | (x e. z /\ (F"z) (_ y)} = {z e. J | (x e. z /\ z (_ (`'F"y))})
15	14	unieqd 2512	. . . . . . 7 |- (F:X-->Y -> U.{z e. J | (x e. z /\ (F"z) (_ y)} = U.{z e. J | (x e. z /\ z (_ (`'F"y))})
16	15	adantr 389	. . . . . 6 |- ((F:X-->Y /\ x e. (`'F"y)) -> U.{z e. J | (x e. z /\ (F"z) (_ y)} = U.{z e. J | (x e. z /\ z (_ (`'F"y))})
17	16	iuneq2dv 2582	. . . . 5 |- (F:X-->Y -> U_x e. (`'F"y)U.{z e. J | (x e. z /\ (F"z) (_ y)} = U_x e. (`'F"y)U.{z e. J | (x e. z /\ z (_ (`'F"y))})
18	17	adantr 389	. . . 4 |- ((F:X-->Y /\ A.x e. X ((F` x) e. y -> E.z e. J (x e. z /\ (F"z) (_ y))) -> U_x e. (`'F"y)U.{z e. J | (x e. z /\ (F"z) (_ y)} = U_x e. (`'F"y)U.{z e. J | (x e. z /\ z (_ (`'F"y))})
19		iunss 2591	. . . . . . 7 |- (U_x e. (`'F"y)U.{z e. J | (x e. z /\ z (_ (`'F"y))} (_ (`'F"y) <-> A.x e. (`'F"y)U.{z e. J | (x e. z /\ z (_ (`'F"y))} (_ (`'F"y))
20		cncnplem1 7774	. . . . . . . 8 |- U.{z e. J | (x e. z /\ z (_ (`'F"y))} (_ (`'F"y)
21	20	a1i 8	. . . . . . 7 |- (x e. (`'F"y) -> U.{z e. J | (x e. z /\ z (_ (`'F"y))} (_ (`'F"y))
22	19, 21	mprgbir 1701	. . . . . 6 |- U_x e. (`'F"y)U.{z e. J | (x e. z /\ z (_ (`'F"y))} (_ (`'F"y)
23	22	a1i 8	. . . . 5 |- ((F:X-->Y /\ A.x e. X ((F` x) e. y -> E.z e. J (x e. z /\ (F"z) (_ y))) -> U_x e. (`'F"y)U.{z e. J | (x e. z /\ z (_ (`'F"y))} (_ (`'F"y))
24		cnvimass 3423	. . . . . . . . . . 11 |- (`'F"y) (_ dom F
25	24	sseli 2065	. . . . . . . . . 10 |- (x e. (`'F"y) -> x e. dom F)
26		fvimacnv 3805	. . . . . . . . . . . . . . 15 |- ((Fun F /\ x e. dom F) -> ((F` x) e. y <-> x e. (`'F"y)))
27	26, 8	sylan 448	. . . . . . . . . . . . . 14 |- ((F:X-->Y /\ x e. dom F) -> ((F` x) e. y <-> x e. (`'F"y)))
28	27	biimprd 154	. . . . . . . . . . . . 13 |- ((F:X-->Y /\ x e. dom F) -> (x e. (`'F"y) -> (F` x) e. y))
29	9	anbi2d 616	. . . . . . . . . . . . . . . . . . . . 21 |- ((F:X-->Y /\ z (_ dom F) -> ((x e. z /\ (F"z) (_ y) <-> (x e. z /\ z (_ (`'F"y))))
30		pm4.24 433	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. z <-> (x e. z /\ x e. z))
31	30	anbi1i 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. z /\ z (_ (`'F"y)) <-> ((x e. z /\ x e. z) /\ z (_ (`'F"y)))
32		anass 439	. . . . . . . . . . . . . . . . . . . . . 22 |- (((x e. z /\ x e. z) /\ z (_ (`'F"y)) <-> (x e. z /\ (x e. z /\ z (_ (`'F"y))))
33	31, 32	bitr 173	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. z /\ z (_ (`'F"y)) <-> (x e. z /\ (x e. z /\ z (_ (`'F"y))))
34	29, 33	syl6bb 536	. . . . . . . . . . . . . . . . . . . 20 |- ((F:X-->Y /\ z (_ dom F) -> ((x e. z /\ (F"z) (_ y) <-> (x e. z /\ (x e. z /\ z (_ (`'F"y)))))
35	34	ex 373	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->Y -> (z (_ dom F -> ((x e. z /\ (F"z) (_ y) <-> (x e. z /\ (x e. z /\ z (_ (`'F"y))))))
36	6, 35	syld 27	. . . . . . . . . . . . . . . . . 18 |- (F:X-->Y -> (z e. J -> ((x e. z /\ (F"z) (_ y) <-> (x e. z /\ (x e. z /\ z (_ (`'F"y))))))
37	36	imp 350	. . . . . . . . . . . . . . . . 17 |- ((F:X-->Y /\ z e. J) -> ((x e. z /\ (F"z) (_ y) <-> (x e. z /\ (x e. z /\ z (_ (`'F"y)))))
38	37	rexbidva 1660	. . . . . . . . . . . . . . . 16 |- (F:X-->Y -> (E.z e. J (x e. z /\ (F"z) (_ y) <-> E.z e. J (x e. z /\ (x e. z /\ z (_ (`'F"y)))))
39		elunirab 2514	. . . . . . . . . . . . . . . 16 |- (x e. U.{z e. J | (x e. z /\ z (_ (`'F"y))} <-> E.z e. J (x e. z /\ (x e. z /\ z (_ (`'F"y))))
40	38, 39	syl6bbr 538	. . . . . . . . . . . . . . 15 |- (F:X-->Y -> (E.z e. J (x e. z /\ (F"z) (_ y) <-> x e. U.{z e. J | (x e. z /\ z (_ (`'F"y))}))
41	40	biimpd 153	. . . . . . . . . . . . . 14 |- (F:X-->Y -> (E.z e. J (x e. z /\ (F"z) (_ y) -> x e. U.{z e. J | (x e. z /\ z (_ (`'F"y))}))
42	41	adantr 389	. . . . . . . . . . . . 13 |- ((F:X-->Y /\ x e. dom F) -> (E.z e. J (x e. z /\ (F"z) (_ y) -> x e. U.{z e. J | (x e. z /\ z (_ (`'F"y))}))
43	28, 42	imim12d 29	. . . . . . . . . . . 12 |- ((F:X-->Y /\ x e. dom F) -> (((F` x) e. y -> E.z e. J (x e. z /\ (F"z) (_ y)) -> (x e. (`'F"y) -> x e. U.{z e. J | (x e. z /\ z (_ (`'F"y))})))
44	43	ex 373	. . . . . . . . . . 11 |- (F:X-->Y -> (x e. dom F -> (((F` x) e. y -> E.z e. J (x e. z /\ (F"z) (_ y)) -> (x e. (`'F"y) -> x e. U.{z e. J | (x e. z /\ z (_ (`'F"y))}))))
45	44	com14 38	. . . . . . . . . 10 |- (x e. (`'F"y) -> (x e. dom F -> (((F` x) e. y -> E.z e. J (x e. z /\ (F"z) (_ y)) -> (F:X-->Y -> x e. U.{z e. J | (x e. z /\ z (_ (`'F"y))}))))
46	25, 45	mpd 26	. . . . . . . . 9 |- (x e. (`'F"y) -> (((F` x) e. y -> E.z e. J (x e. z /\ (F"z) (_ y)) -> (