Theorem fisub 14924

Description: If a set has the finite intersection property, its subsets have also this property.

Hypotheses

Ref	Expression
fisub.1	|- B = {z | E.y(y C_ A /\ y e. Fin /\ z = |^|y)}
fisub.2	|- D = {z | E.y(y C_ C /\ y e. Fin /\ z = |^|y)}

Assertion

Ref	Expression
fisub	|- (C C_ A -> (-. (/) e. B -> -. (/) e. D))

Distinct variable groups:   y,A,z   y,B   y,C,z

Proof of Theorem fisub

Step	Hyp	Ref	Expression
1		sstr 2625	. . . . . . . . 9 |- ((y C_ C /\ C C_ A) -> y C_ A)
2		0ex 3446	. . . . . . . . . . . . 13 |- (/) e. _V
3		eqeq1 1890	. . . . . . . . . . . . . . 15 |- (z = (/) -> (z = |^|y <-> (/) = |^|y))
4	3	3anbi3d 1174	. . . . . . . . . . . . . 14 |- (z = (/) -> ((y C_ A /\ y e. Fin /\ z = |^|y) <-> (y C_ A /\ y e. Fin /\ (/) = |^|y)))
5	4	exbidv 1657	. . . . . . . . . . . . 13 |- (z = (/) -> (E.y(y C_ A /\ y e. Fin /\ z = |^|y) <-> E.y(y C_ A /\ y e. Fin /\ (/) = |^|y)))
6		fisub.1	. . . . . . . . . . . . 13 |- B = {z | E.y(y C_ A /\ y e. Fin /\ z = |^|y)}
7	2, 5, 6	elab2 2407	. . . . . . . . . . . 12 |- ((/) e. B <-> E.y(y C_ A /\ y e. Fin /\ (/) = |^|y))
8	7	biimpri 169	. . . . . . . . . . 11 |- (E.y(y C_ A /\ y e. Fin /\ (/) = |^|y) -> (/) e. B)
9	8	19.23bi 1414	. . . . . . . . . 10 |- ((y C_ A /\ y e. Fin /\ (/) = |^|y) -> (/) e. B)
10	9	3exp 1066	. . . . . . . . 9 |- (y C_ A -> (y e. Fin -> ((/) = |^|y -> (/) e. B)))
11	1, 10	syl 12	. . . . . . . 8 |- ((y C_ C /\ C C_ A) -> (y e. Fin -> ((/) = |^|y -> (/) e. B)))
12	11	expcom 403	. . . . . . 7 |- (C C_ A -> (y C_ C -> (y e. Fin -> ((/) = |^|y -> (/) e. B))))
13	12	com4l 43	. . . . . 6 |- (y C_ C -> (y e. Fin -> ((/) = |^|y -> (C C_ A -> (/) e. B))))
14	13	3imp 1061	. . . . 5 |- ((y C_ C /\ y e. Fin /\ (/) = |^|y) -> (C C_ A -> (/) e. B))
15	14	19.23aiv 1674	. . . 4 |- (E.y(y C_ C /\ y e. Fin /\ (/) = |^|y) -> (C C_ A -> (/) e. B))
16	15	com12 14	. . 3 |- (C C_ A -> (E.y(y C_ C /\ y e. Fin /\ (/) = |^|y) -> (/) e. B))
17	3	3anbi3d 1174	. . . . 5 |- (z = (/) -> ((y C_ C /\ y e. Fin /\ z = |^|y) <-> (y C_ C /\ y e. Fin /\ (/) = |^|y)))
18	17	exbidv 1657	. . . 4 |- (z = (/) -> (E.y(y C_ C /\ y e. Fin /\ z = |^|y) <-> E.y(y C_ C /\ y e. Fin /\ (/) = |^|y)))
19		fisub.2	. . . 4 |- D = {z | E.y(y C_ C /\ y e. Fin /\ z = |^|y)}
20	2, 18, 19	elab2 2407	. . 3 |- ((/) e. D <-> E.y(y C_ C /\ y e. Fin /\ (/) = |^|y))
21	16, 20	syl5ib 223	. 2 |- (C C_ A -> ((/) e. D -> (/) e. B))
22	21	con3d 111	1 |- (C C_ A -> (-. (/) e. B -> -. (/) e. D))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   C_ wss 2593  (/)c0 2875  |^|cint 3214  Fincfn 5426

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-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-nul 3445

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-in 2603  df-ss 2605  df-nul 2876

Copyright terms: Public domain