Theorem fbunfip 10282

Description: A helpful lemma for showing that certain sets generate filters. (Contributed by Jeff Hankins, 3-Sep-2009.)

Assertion

Ref	Expression
fbunfip	|- ((F e. fBas /\ G e. fBas) -> ((/) e/ ( fi ` (F u. G)) <-> A.x e. F A.y e. G (x i^i y) =/= (/)))

Distinct variable groups:   x,y,F   x,G,y

Proof of Theorem fbunfip

Step	Hyp	Ref	Expression
1		unexg 3798	. . . . . . 7 |- ((F e. fBas /\ G e. fBas) -> (F u. G) e. _V)
2		fiv 10212	. . . . . . 7 |- ((F u. G) e. _V -> ( fi ` (F u. G)) = {u | E.v(v C_ (F u. G) /\ v e. Fin /\ u = |^|v)})
3	1, 2	syl 12	. . . . . 6 |- ((F e. fBas /\ G e. fBas) -> ( fi ` (F u. G)) = {u | E.v(v C_ (F u. G) /\ v e. Fin /\ u = |^|v)})
4	3	eleq2d 1964	. . . . 5 |- ((F e. fBas /\ G e. fBas) -> ((/) e. ( fi ` (F u. G)) <-> (/) e. {u | E.v(v C_ (F u. G) /\ v e. Fin /\ u = |^|v)}))
5		0ex 3446	. . . . . 6 |- (/) e. _V
6		eqeq1 1890	. . . . . . . 8 |- (u = (/) -> (u = |^|v <-> (/) = |^|v))
7	6	3anbi3d 1174	. . . . . . 7 |- (u = (/) -> ((v C_ (F u. G) /\ v e. Fin /\ u = |^|v) <-> (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v)))
8	7	exbidv 1657	. . . . . 6 |- (u = (/) -> (E.v(v C_ (F u. G) /\ v e. Fin /\ u = |^|v) <-> E.v(v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v)))
9	5, 8	elab 2403	. . . . 5 |- ((/) e. {u | E.v(v C_ (F u. G) /\ v e. Fin /\ u = |^|v)} <-> E.v(v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v))
10	4, 9	syl6bb 595	. . . 4 |- ((F e. fBas /\ G e. fBas) -> ((/) e. ( fi ` (F u. G)) <-> E.v(v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v)))
11	10	notbid 673	. . 3 |- ((F e. fBas /\ G e. fBas) -> (-. (/) e. ( fi ` (F u. G)) <-> -. E.v(v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v)))
12		df-nel 2020	. . 3 |- ((/) e/ ( fi ` (F u. G)) <-> -. (/) e. ( fi ` (F u. G)))
13		alnex 1380	. . 3 |- (A.v -. (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v) <-> -. E.v(v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v))
14	11, 12, 13	3bitr4g 614	. 2 |- ((F e. fBas /\ G e. fBas) -> ((/) e/ ( fi ` (F u. G)) <-> A.v -. (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v)))
15		ssun1 2767	. . . . . . . . . . . 12 |- F C_ (F u. G)
16	15	a1i 8	. . . . . . . . . . 11 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> F C_ (F u. G))
17		simprl 450	. . . . . . . . . . 11 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> x e. F)
18	16, 17	sseldd 2620	. . . . . . . . . 10 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> x e. (F u. G))
19		ssun2 2768	. . . . . . . . . . . 12 |- G C_ (F u. G)
20	19	a1i 8	. . . . . . . . . . 11 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> G C_ (F u. G))
21		simprr 451	. . . . . . . . . . 11 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> y e. G)
22	20, 21	sseldd 2620	. . . . . . . . . 10 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> y e. (F u. G))
23	18, 22	jca 310	. . . . . . . . 9 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> (x e. (F u. G) /\ y e. (F u. G)))
24		visset 2295	. . . . . . . . . 10 |- x e. _V
25		visset 2295	. . . . . . . . . 10 |- y e. _V
26	24, 25	prss 3138	. . . . . . . . 9 |- ((x e. (F u. G) /\ y e. (F u. G)) <-> {x, y} C_ (F u. G))
27	23, 26	sylib 215	. . . . . . . 8 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> {x, y} C_ (F u. G))
28		prfi 5647	. . . . . . . 8 |- {x, y} e. Fin
29	27, 28	jctir 317	. . . . . . 7 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> ({x, y} C_ (F u. G) /\ {x, y} e. Fin))
30		pm2.27 76	. . . . . . . . 9 |- (({x, y} C_ (F u. G) /\ {x, y} e. Fin) -> ((({x, y} C_ (F u. G) /\ {x, y} e. Fin) -> -. (/) = |^|{x, y}) -> -. (/) = |^|{x, y}))
31		necom 2094	. . . . . . . . . . . 12 |- ((/) =/= |^|{x, y} <-> |^|{x, y} =/= (/))
32		df-ne 2019	. . . . . . . . . . . 12 |- ((/) =/= |^|{x, y} <-> -. (/) = |^|{x, y})
33	24, 25	intpr 3250	. . . . . . . . . . . . 13 |- |^|{x, y} = (x i^i y)
34	33	neeq1i 2026	. . . . . . . . . . . 12 |- (|^|{x, y} =/= (/) <-> (x i^i y) =/= (/))
35	31, 32, 34	3bitr3i 198	. . . . . . . . . . 11 |- (-. (/) = |^|{x, y} <-> (x i^i y) =/= (/))
36	35	biimpi 168	. . . . . . . . . 10 |- (-. (/) = |^|{x, y} -> (x i^i y) =/= (/))
37	36	a1d 15	. . . . . . . . 9 |- (-. (/) = |^|{x, y} -> (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> (x i^i y) =/= (/)))
38	30, 37	syl6 25	. . . . . . . 8 |- (({x, y} C_ (F u. G) /\ {x, y} e. Fin) -> ((({x, y} C_ (F u. G) /\ {x, y} e. Fin) -> -. (/) = |^|{x, y}) -> (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> (x i^i y) =/= (/))))
39	38	com3r 39	. . . . . . 7 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> (({x, y} C_ (F u. G) /\ {x, y} e. Fin) -> ((({x, y} C_ (F u. G) /\ {x, y} e. Fin) -> -. (/) = |^|{x, y}) -> (x i^i y) =/= (/))))
40	29, 39	mpd 29	. . . . . 6 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> ((({x, y} C_ (F u. G) /\ {x, y} e. Fin) -> -. (/) = |^|{x, y}) -> (x i^i y) =/= (/)))
41		df-3an 860	. . . . . . . 8 |- (({x, y} C_ (F u. G) /\ {x, y} e. Fin /\ (/) = |^|{x, y}) <-> (({x, y} C_ (F u. G) /\ {x, y} e. Fin) /\ (/) = |^|{x, y}))
42	41	notbii 204	. . . . . . 7 |- (-. ({x, y} C_ (F u. G) /\ {x, y} e. Fin /\ (/) = |^|{x, y}) <-> -. (({x, y} C_ (F u. G) /\ {x, y} e. Fin) /\ (/) = |^|{x, y}))
43		imnan 261	. . . . . . 7 |- ((({x, y} C_ (F u. G) /\ {x, y} e. Fin) -> -. (/) = |^|{x, y}) <-> -. (({x, y} C_ (F u. G) /\ {x, y} e. Fin) /\ (/) = |^|{x, y}))
44	42, 43	bitr4i 193	. . . . . 6 |- (-. ({x, y} C_ (F u. G) /\ {x, y} e. Fin /\ (/) = |^|{x, y}) <-> (({x, y} C_ (F u. G) /\ {x, y} e. Fin) -> -. (/) = |^|{x, y}))
45	40, 44	syl5ib 223	. . . . 5 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> (-. ({x, y} C_ (F u. G) /\ {x, y} e. Fin /\ (/) = |^|{x, y}) -> (x i^i y) =/= (/)))
46		zfpair2 3525	. . . . . 6 |- {x, y} e. _V
47		sseq1 2637	. . . . . . . 8 |- (v = {x, y} -> (v C_ (F u. G) <-> {x, y} C_ (F u. G)))
48		eleq1 1957	. . . . . . . 8 |- (v = {x, y} -> (v e. Fin <-> {x, y} e. Fin))
49		inteq 3217	. . . . . . . . 9 |- (v = {x, y} -> |^|v = |^|{x, y})
50	49	eqeq2d 1895	. . . . . . . 8 |- (v = {x, y} -> ((/) = |^|v <-> (/) = |^|{x, y}))
51	47, 48, 50	3anbi123d 1168	. . . . . . 7 |- (v = {x, y} -> ((v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v) <-> ({x, y} C_ (F u. G) /\ {x, y} e. Fin /\ (/) = |^|{x, y})))
52	51	notbid 673	. . . . . 6 |- (v = {x, y} -> (-. (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v) <-> -. ({x, y} C_ (F u. G) /\ {x, y} e. Fin /\ (/) = |^|{x, y})))
53	46, 52	cla4v 2370	. . . . 5 |- (A.v -. (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v) -> -. ({x, y} C_ (F u. G) /\ {x, y} e. Fin /\ (/) = |^|{x, y}))
54	45, 53	syl5 20	. . . 4 |- (((F e. fBas /\ G e. fBas) /\ (x e. F /\ y e. G)) -> (A.v -. (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v) -> (x i^i y) =/= (/)))
55	54	r19.21advva 2185	. . 3 |- ((F e. fBas /\ G e. fBas) -> (A.v -. (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v) -> A.x e. F A.y e. G (x i^i y) =/= (/)))
56		inss2 2813	. . . . . . . . . . . . . . . . 17 |- (v i^i F) C_ F
57		fbssint 10279	. . . . . . . . . . . . . . . . 17 |- ((F e. fBas /\ (v i^i F) C_ F /\ (v i^i F) e. Fin) -> E.r e. F r C_ |^|(v i^i F))
58	56, 57	mp3an2 1179	. . . . . . . . . . . . . . . 16 |- ((F e. fBas /\ (v i^i F) e. Fin) -> E.r e. F r C_ |^|(v i^i F))
59	58	ad2ant2r 445	. . . . . . . . . . . . . . 15 |- (((F e. fBas /\ G e. fBas) /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin)) -> E.r e. F r C_ |^|(v i^i F))
60		inss2 2813	. . . . . . . . . . . . . . . . 17 |- (v i^i G) C_ G
61		fbssint 10279	. . . . . . . . . . . . . . . . 17 |- ((G e. fBas /\ (v i^i G) C_ G /\ (v i^i G) e. Fin) -> E.s e. G s C_ |^|(v i^i G))
62	60, 61	mp3an2 1179	. . . . . . . . . . . . . . . 16 |- ((G e. fBas /\ (v i^i G) e. Fin) -> E.s e. G s C_ |^|(v i^i G))
63	62	ad2ant2l 444	. . . . . . . . . . . . . . 15 |- (((F e. fBas /\ G e. fBas) /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin)) -> E.s e. G s C_ |^|(v i^i G))
64	59, 63	jca 310	. . . . . . . . . . . . . 14 |- (((F e. fBas /\ G e. fBas) /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin)) -> (E.r e. F r C_ |^|(v i^i F) /\ E.s e. G s C_ |^|(v i^i G)))
65		ss2in 2820	. . . . . . . . . . . . . . . . . . . . 21 |- ((r C_ |^|(v i^i F) /\ s C_ |^|(v i^i G)) -> (r i^i s) C_ (|^|(v i^i F) i^i |^|(v i^i G)))
66	65	ad2antll 443	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. fBas /\ G e. fBas) /\ ((r e. F /\ s e. G) /\ (r C_ |^|(v i^i F) /\ s C_ |^|(v i^i G)))) -> (r i^i s) C_ (|^|(v i^i F) i^i |^|(v i^i G)))
67		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = r -> (x i^i y) = (r i^i y))
68	67	neeq1d 2028	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = r -> ((x i^i y) =/= (/) <-> (r i^i y) =/= (/)))
69		ineq2 2790	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = s -> (r i^i y) = (r i^i s))
70	69	neeq1d 2028	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = s -> ((r i^i y) =/= (/) <-> (r i^i s) =/= (/)))
71	68, 70	rcla42v 2384	. . . . . . . . . . . . . . . . . . . . 21 |- ((r e. F /\ s e. G) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> (r i^i s) =/= (/)))
72	71	ad2antrl 442	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. fBas /\ G e. fBas) /\ ((r e. F /\ s e. G) /\ (r C_ |^|(v i^i F) /\ s C_ |^|(v i^i G)))) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> (r i^i s) =/= (/)))
73		ssn0 2905	. . . . . . . . . . . . . . . . . . . . 21 |- (((r i^i s) C_ (|^|(v i^i F) i^i |^|(v i^i G)) /\ (r i^i s) =/= (/)) -> (|^|(v i^i F) i^i |^|(v i^i G)) =/= (/))
74	73	ex 402	. . . . . . . . . . . . . . . . . . . 20 |- ((r i^i s) C_ (|^|(v i^i F) i^i |^|(v i^i G)) -> ((r i^i s) =/= (/) -> (|^|(v i^i F) i^i |^|(v i^i G)) =/= (/)))
75	66, 72, 74	sylsyld 32	. . . . . . . . . . . . . . . . . . 19 |- (((F e. fBas /\ G e. fBas) /\ ((r e. F /\ s e. G) /\ (r C_ |^|(v i^i F) /\ s C_ |^|(v i^i G)))) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> (|^|(v i^i F) i^i |^|(v i^i G)) =/= (/)))
76	75	exp32 408	. . . . . . . . . . . . . . . . . 18 |- ((F e. fBas /\ G e. fBas) -> ((r e. F /\ s e. G) -> ((r C_ |^|(v i^i F) /\ s C_ |^|(v i^i G)) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> (|^|(v i^i F) i^i |^|(v i^i G)) =/= (/)))))
77	76	com3l 38	. . . . . . . . . . . . . . . . 17 |- ((r e. F /\ s e. G) -> ((r C_ |^|(v i^i F) /\ s C_ |^|(v i^i G)) -> ((F e. fBas /\ G e. fBas) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> (|^|(v i^i F) i^i |^|(v i^i G)) =/= (/)))))
78	77	r19.23aivv 2217	. . . . . . . . . . . . . . . 16 |- (E.r e. F E.s e. G (r C_ |^|(v i^i F) /\ s C_ |^|(v i^i G)) -> ((F e. fBas /\ G e. fBas) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> (|^|(v i^i F) i^i |^|(v i^i G)) =/= (/))))
79	78	impcom 378	. . . . . . . . . . . . . . 15 |- (((F e. fBas /\ G e. fBas) /\ E.r e. F E.s e. G (r C_ |^|(v i^i F) /\ s C_ |^|(v i^i G))) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> (|^|(v i^i F) i^i |^|(v i^i G)) =/= (/)))
80		reeanv 2249	. . . . . . . . . . . . . . 15 |- (E.r e. F E.s e. G (r C_ |^|(v i^i F) /\ s C_ |^|(v i^i G)) <-> (E.r e. F r C_ |^|(v i^i F) /\ E.s e. G s C_ |^|(v i^i G)))
81	79, 80	sylan2br 502	. . . . . . . . . . . . . 14 |- (((F e. fBas /\ G e. fBas) /\ (E.r e. F r C_ |^|(v i^i F) /\ E.s e. G s C_ |^|(v i^i G))) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> (|^|(v i^i F) i^i |^|(v i^i G)) =/= (/)))
82	64, 81	syldan 516	. . . . . . . . . . . . 13 |- (((F e. fBas /\ G e. fBas) /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin)) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> (|^|(v i^i F) i^i |^|(v i^i G)) =/= (/)))
83		necom 2094	. . . . . . . . . . . . . 14 |- ((|^|(v i^i F) i^i |^|(v i^i G)) =/= (/) <-> (/) =/= (|^|(v i^i F) i^i |^|(v i^i G)))
84		df-ne 2019	. . . . . . . . . . . . . 14 |- ((/) =/= (|^|(v i^i F) i^i |^|(v i^i G)) <-> -. (/) = (|^|(v i^i F) i^i |^|(v i^i G)))
85	83, 84	bitri 190	. . . . . . . . . . . . 13 |- ((|^|(v i^i F) i^i |^|(v i^i G)) =/= (/) <-> -. (/) = (|^|(v i^i F) i^i |^|(v i^i G)))
86	82, 85	syl6ib 229	. . . . . . . . . . . 12 |- (((F e. fBas /\ G e. fBas) /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin)) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> -. (/) = (|^|(v i^i F) i^i |^|(v i^i G))))
87	86	adantrl 430	. . . . . . . . . . 11 |- (((F e. fBas /\ G e. fBas) /\ (((v i^i F) u. (v i^i G)) = v /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin))) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> -. (/) = (|^|(v i^i F) i^i |^|(v i^i G))))
88		intun 3249	. . . . . . . . . . . . 13 |- |^|((v i^i F) u. (v i^i G)) = (|^|(v i^i F) i^i |^|(v i^i G))
89	88	eqeq2i 1894	. . . . . . . . . . . 12 |- ((/) = |^|((v i^i F) u. (v i^i G)) <-> (/) = (|^|(v i^i F) i^i |^|(v i^i G)))
90	89	notbii 204	. . . . . . . . . . 11 |- (-. (/) = |^|((v i^i F) u. (v i^i G)) <-> -. (/) = (|^|(v i^i F) i^i |^|(v i^i G)))
91	87, 90	syl6ibr 230	. . . . . . . . . 10 |- (((F e. fBas /\ G e. fBas) /\ (((v i^i F) u. (v i^i G)) = v /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin))) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> -. (/) = |^|((v i^i F) u. (v i^i G))))
92		simprl 450	. . . . . . . . . . . . 13 |- (((F e. fBas /\ G e. fBas) /\ (((v i^i F) u. (v i^i G)) = v /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin))) -> ((v i^i F) u. (v i^i G)) = v)
93	92	inteqd 3219	. . . . . . . . . . . 12 |- (((F e. fBas /\ G e. fBas) /\ (((v i^i F) u. (v i^i G)) = v /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin))) -> |^|((v i^i F) u. (v i^i G)) = |^|v)
94	93	eqeq2d 1895	. . . . . . . . . . 11 |- (((F e. fBas /\ G e. fBas) /\ (((v i^i F) u. (v i^i G)) = v /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin))) -> ((/) = |^|((v i^i F) u. (v i^i G)) <-> (/) = |^|v))
95	94	notbid 673	. . . . . . . . . 10 |- (((F e. fBas /\ G e. fBas) /\ (((v i^i F) u. (v i^i G)) = v /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin))) -> (-. (/) = |^|((v i^i F) u. (v i^i G)) <-> -. (/) = |^|v))
96	91, 95	sylibd 219	. . . . . . . . 9 |- (((F e. fBas /\ G e. fBas) /\ (((v i^i F) u. (v i^i G)) = v /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin))) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> -. (/) = |^|v))
97	96	ex 402	. . . . . . . 8 |- ((F e. fBas /\ G e. fBas) -> ((((v i^i F) u. (v i^i G)) = v /\ ((v i^i F) e. Fin /\ (v i^i G) e. Fin)) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> -. (/) = |^|v)))
98		inss1 2812	. . . . . . . . . 10 |- (v i^i F) C_ v
99		ssfi 5630	. . . . . . . . . 10 |- ((v e. Fin /\ (v i^i F) C_ v) -> (v i^i F) e. Fin)
100	98, 99	mpan2 760	. . . . . . . . 9 |- (v e. Fin -> (v i^i F) e. Fin)
101		inss1 2812	. . . . . . . . . 10 |- (v i^i G) C_ v
102		ssfi 5630	. . . . . . . . . 10 |- ((v e. Fin /\ (v i^i G) C_ v) -> (v i^i G) e. Fin)
103	101, 102	mpan2 760	. . . . . . . . 9 |- (v e. Fin -> (v i^i G) e. Fin)
104	100, 103	jca 310	. . . . . . . 8 |- (v e. Fin -> ((v i^i F) e. Fin /\ (v i^i G) e. Fin))
105	97, 104	sylan2i 514	. . . . . . 7 |- ((F e. fBas /\ G e. fBas) -> ((((v i^i F) u. (v i^i G)) = v /\ v e. Fin) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> -. (/) = |^|v)))
106		df-ss 2605	. . . . . . . . 9 |- (v C_ (F u. G) <-> (v i^i (F u. G)) = v)
107		indi 2838	. . . . . . . . . 10 |- (v i^i (F u. G)) = ((v i^i F) u. (v i^i G))
108	107	eqeq1i 1891	. . . . . . . . 9 |- ((v i^i (F u. G)) = v <-> ((v i^i F) u. (v i^i G)) = v)
109	106, 108	bitri 190	. . . . . . . 8 |- (v C_ (F u. G) <-> ((v i^i F) u. (v i^i G)) = v)
110	109	anbi1i 539	. . . . . . 7 |- ((v C_ (F u. G) /\ v e. Fin) <-> (((v i^i F) u. (v i^i G)) = v /\ v e. Fin))
111	105, 110	syl5ib 223	. . . . . 6 |- ((F e. fBas /\ G e. fBas) -> ((v C_ (F u. G) /\ v e. Fin) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> -. (/) = |^|v)))
112	111	com23 36	. . . . 5 |- ((F e. fBas /\ G e. fBas) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> ((v C_ (F u. G) /\ v e. Fin) -> -. (/) = |^|v)))
113		imnan 261	. . . . . 6 |- (((v C_ (F u. G) /\ v e. Fin) -> -. (/) = |^|v) <-> -. ((v C_ (F u. G) /\ v e. Fin) /\ (/) = |^|v))
114		df-3an 860	. . . . . . 7 |- ((v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v) <-> ((v C_ (F u. G) /\ v e. Fin) /\ (/) = |^|v))
115	114	notbii 204	. . . . . 6 |- (-. (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v) <-> -. ((v C_ (F u. G) /\ v e. Fin) /\ (/) = |^|v))
116	113, 115	bitr4i 193	. . . . 5 |- (((v C_ (F u. G) /\ v e. Fin) -> -. (/) = |^|v) <-> -. (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v))
117	112, 116	syl6ib 229	. . . 4 |- ((F e. fBas /\ G e. fBas) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> -. (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v)))
118	117	19.21adv 1666	. . 3 |- ((F e. fBas /\ G e. fBas) -> (A.x e. F A.y e. G (x i^i y) =/= (/) -> A.v -. (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v)))
119	55, 118	impbid 574	. 2 |- ((F e. fBas /\ G e. fBas) -> (A.v -. (v C_ (F u. G) /\ v e. Fin /\ (/) = |^|v) <-> A.x e. F A.y e. G (x i^i y) =/= (/)))
120	14, 119	bitrd 587	1 |- ((F e. fBas /\ G e. fBas) -> ((/) e/ ( fi ` (F u. G)) <-> A.x e. F A.y e. G (x i^i y) =/= (/)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   =/= wne 2017   e/ wnel 2018  A.wral 2105  E.wrex 2106  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  {cpr 3045  |^|cint 3214  ` cfv 3998  Fincfn 5426   fi cfi 10210  fBascfbas 10257

This theorem is referenced by:  hausfillim 10303  isufil2 15565  ufileulem 15572  ufileu 15573  filufint 15574  flimcls 15588  fmfnfm 15598  fclsfnflim 15614  flimfnfcls 15615

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-rep 3428  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-3or 859  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-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-fin 5430  df-fi 10211  df-fbas 10259

Copyright terms: Public domain