Theorem rcfpfillem4 10566

Description: Lemma for rcfpfil 10569.

Assertion

Ref	Expression
rcfpfillem4	|- (A e. B -> A.u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}A.v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} (u i^i v) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})

Distinct variable groups:   A,b,u,v,x   u,B,v

Proof of Theorem rcfpfillem4

Step	Hyp	Ref	Expression
1		an6 904	. . . . . . . . . . . . . 14 |- (((a (_ A /\ a e. Fin /\ u = (A \ a)) /\ (c (_ A /\ c e. Fin /\ v = (A \ c))) <-> ((a (_ A /\ c (_ A) /\ (a e. Fin /\ c e. Fin) /\ (u = (A \ a) /\ v = (A \ c))))
2		unss 2207	. . . . . . . . . . . . . . . 16 |- ((a (_ A /\ c (_ A) <-> (a u. c) (_ A)
3	2	biimp 151	. . . . . . . . . . . . . . 15 |- ((a (_ A /\ c (_ A) -> (a u. c) (_ A)
4		unfi 4563	. . . . . . . . . . . . . . 15 |- ((a e. Fin /\ c e. Fin) -> (a u. c) e. Fin)
5		ineq12 2215	. . . . . . . . . . . . . . . 16 |- ((u = (A \ a) /\ v = (A \ c)) -> (u i^i v) = ((A \ a) i^i (A \ c)))
6		difundi 2260	. . . . . . . . . . . . . . . 16 |- (A \ (a u. c)) = ((A \ a) i^i (A \ c))
7	5, 6	syl6eqr 1528	. . . . . . . . . . . . . . 15 |- ((u = (A \ a) /\ v = (A \ c)) -> (u i^i v) = (A \ (a u. c)))
8	3, 4, 7	3anim123i 823	. . . . . . . . . . . . . 14 |- (((a (_ A /\ c (_ A) /\ (a e. Fin /\ c e. Fin) /\ (u = (A \ a) /\ v = (A \ c))) -> ((a u. c) (_ A /\ (a u. c) e. Fin /\ (u i^i v) = (A \ (a u. c))))
9	1, 8	sylbi 199	. . . . . . . . . . . . 13 |- (((a (_ A /\ a e. Fin /\ u = (A \ a)) /\ (c (_ A /\ c e. Fin /\ v = (A \ c))) -> ((a u. c) (_ A /\ (a u. c) e. Fin /\ (u i^i v) = (A \ (a u. c))))
10	9	expcom 374	. . . . . . . . . . . 12 |- ((c (_ A /\ c e. Fin /\ v = (A \ c)) -> ((a (_ A /\ a e. Fin /\ u = (A \ a)) -> ((a u. c) (_ A /\ (a u. c) e. Fin /\ (u i^i v) = (A \ (a u. c)))))
11		visset 1816	. . . . . . . . . . . . . 14 |- a e. V
12		visset 1816	. . . . . . . . . . . . . 14 |- c e. V
13	11, 12	unex 2878	. . . . . . . . . . . . 13 |- (a u. c) e. V
14		sseq1 2085	. . . . . . . . . . . . . 14 |- (b = (a u. c) -> (b (_ A <-> (a u. c) (_ A))
15		eleq1 1537	. . . . . . . . . . . . . 14 |- (b = (a u. c) -> (b e. Fin <-> (a u. c) e. Fin))
16		difeq2 2157	. . . . . . . . . . . . . . 15 |- (b = (a u. c) -> (A \ b) = (A \ (a u. c)))
17	16	eqeq2d 1489	. . . . . . . . . . . . . 14 |- (b = (a u. c) -> ((u i^i v) = (A \ b) <-> (u i^i v) = (A \ (a u. c))))
18	14, 15, 17	3anbi123d 895	. . . . . . . . . . . . 13 |- (b = (a u. c) -> ((b (_ A /\ b e. Fin /\ (u i^i v) = (A \ b)) <-> ((a u. c) (_ A /\ (a u. c) e. Fin /\ (u i^i v) = (A \ (a u. c)))))
19	13, 18	cla4ev 1872	. . . . . . . . . . . 12 |- (((a u. c) (_ A /\ (a u. c) e. Fin /\ (u i^i v) = (A \ (a u. c))) -> E.b(b (_ A /\ b e. Fin /\ (u i^i v) = (A \ b)))
20	10, 19	syl6 22	. . . . . . . . . . 11 |- ((c (_ A /\ c e. Fin /\ v = (A \ c)) -> ((a (_ A /\ a e. Fin /\ u = (A \ a)) -> E.b(b (_ A /\ b e. Fin /\ (u i^i v) = (A \ b))))
21	20	19.23aiv 1297	. . . . . . . . . 10 |- (E.c(c (_ A /\ c e. Fin /\ v = (A \ c)) -> ((a (_ A /\ a e. Fin /\ u = (A \ a)) -> E.b(b (_ A /\ b e. Fin /\ (u i^i v) = (A \ b))))
22	21	com12 11	. . . . . . . . 9 |- ((a (_ A /\ a e. Fin /\ u = (A \ a)) -> (E.c(c (_ A /\ c e. Fin /\ v = (A \ c)) -> E.b(b (_ A /\ b e. Fin /\ (u i^i v) = (A \ b))))
23	22	19.23aiv 1297	. . . . . . . 8 |- (E.a(a (_ A /\ a e. Fin /\ u = (A \ a)) -> (E.c(c (_ A /\ c e. Fin /\ v = (A \ c)) -> E.b(b (_ A /\ b e. Fin /\ (u i^i v) = (A \ b))))
24	23	imp 350	. . . . . . 7 |- ((E.a(a (_ A /\ a e. Fin /\ u = (A \ a)) /\ E.c(c (_ A /\ c e. Fin /\ v = (A \ c))) -> E.b(b (_ A /\ b e. Fin /\ (u i^i v) = (A \ b)))
25		sseq1 2085	. . . . . . . . 9 |- (b = a -> (b (_ A <-> a (_ A))
26		eleq1 1537	. . . . . . . . 9 |- (b = a -> (b e. Fin <-> a e. Fin))
27		difeq2 2157	. . . . . . . . . 10 |- (b = a -> (A \ b) = (A \ a))
28	27	eqeq2d 1489	. . . . . . . . 9 |- (b = a -> (u = (A \ b) <-> u = (A \ a)))
29	25, 26, 28	3anbi123d 895	. . . . . . . 8 |- (b = a -> ((b (_ A /\ b e. Fin /\ u = (A \ b)) <-> (a (_ A /\ a e. Fin /\ u = (A \ a))))
30	29	cbvexv 1317	. . . . . . 7 |- (E.b(b (_ A /\ b e. Fin /\ u = (A \ b)) <-> E.a(a (_ A /\ a e. Fin /\ u = (A \ a)))
31		sseq1 2085	. . . . . . . . 9 |- (b = c -> (b (_ A <-> c (_ A))
32		eleq1 1537	. . . . . . . . 9 |- (b = c -> (b e. Fin <-> c e. Fin))
33		difeq2 2157	. . . . . . . . . 10 |- (b = c -> (A \ b) = (A \ c))
34	33	eqeq2d 1489	. . . . . . . . 9 |- (b = c -> (v = (A \ b) <-> v = (A \ c)))
35	31, 32, 34	3anbi123d 895	. . . . . . . 8 |- (b = c -> ((b (_ A /\ b e. Fin /\ v = (A \ b)) <-> (c (_ A /\ c e. Fin /\ v = (A \ c))))
36	35	cbvexv 1317	. . . . . . 7 |- (E.b(b (_ A /\ b e. Fin /\ v = (A \ b)) <-> E.c(c (_ A /\ c e. Fin /\ v = (A \ c)))
37	24, 30, 36	syl2anb 457	. . . . . 6 |- ((E.b(b (_ A /\ b e. Fin /\ u = (A \ b)) /\ E.b(b (_ A /\ b e. Fin /\ v = (A \ b))) -> E.b(b (_ A /\ b e. Fin /\ (u i^i v) = (A \ b)))
38	37	adantl 390	. . . . 5 |- ((A e. B /\ (E.b(b (_ A /\ b e. Fin /\ u = (A \ b)) /\ E.b(b (_ A /\ b e. Fin /\ v = (A \ b)))) -> E.b(b (_ A /\ b e. Fin /\ (u i^i v) = (A \ b)))
39		visset 1816	. . . . . . 7 |- u e. V
40	39	inex1 2721	. . . . . 6 |- (u i^i v) e. V
41		rcfpfillem1 10563	. . . . . 6 |- ((u i^i v) e. V -> ((u i^i v) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} <-> E.b(b (_ A /\ b e. Fin /\ (u i^i v) = (A \ b))))
42	40, 41	ax-mp 7	. . . . 5 |- ((u i^i v) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} <-> E.b(b (_ A /\ b e. Fin /\ (u i^i v) = (A \ b)))
43	38, 42	sylibr 200	. . . 4 |- ((A e. B /\ (E.b(b (_ A /\ b e. Fin /\ u = (A \ b)) /\ E.b(b (_ A /\ b e. Fin /\ v = (A \ b)))) -> (u i^i v) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
44	43	ex 373	. . 3 |- (A e. B -> ((E.b(b (_ A /\ b e. Fin /\ u = (A \ b)) /\ E.b(b (_ A /\ b e. Fin /\ v = (A \ b))) -> (u i^i v) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}))
45		visset 1816	. . . 4 |- v e. V
46		rcfpfillem1 10563	. . . . 5 |- (u e. V -> (u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} <-> E.b(b (_ A /\ b e. Fin /\ u = (A \ b))))
47		rcfpfillem1 10563	. . . . 5 |- (v e. V -> (v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} <-> E.b(b (_ A /\ b e. Fin /\ v = (A \ b))))
48	46, 47	bi2anan9 634	. . . 4 |- ((u e. V /\ v e. V) -> ((u e. {x | E.b(b (_ A /\ b