Theorem ufinffr 15578

Description: An infinite subset is contained in a free ultrafilter.

Assertion

Ref	Expression
ufinffr	|- ((X e. B /\ A C_ X /\ om ~<_ A) -> E.f e. UFil (X = U.f /\ A e. f /\ |^|f = (/)))

Distinct variable groups:   A,f   B,f   f,X

Proof of Theorem ufinffr

Step	Hyp	Ref	Expression
1		domnsym 5526	. . . . . . . . 9 |- (om ~<_ A -> -. A ~< om)
2	1	3ad2ant3 899	. . . . . . . 8 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> -. A ~< om)
3		dif0 2943	. . . . . . . . . 10 |- (A \ (/)) = A
4	3	eleq1i 1960	. . . . . . . . 9 |- ((A \ (/)) e. Fin <-> A e. Fin)
5		isfinite 5741	. . . . . . . . . 10 |- (A ~< om <-> A e. Fin)
6	5	biimpri 169	. . . . . . . . 9 |- (A e. Fin -> A ~< om)
7	4, 6	sylbi 216	. . . . . . . 8 |- ((A \ (/)) e. Fin -> A ~< om)
8	2, 7	nsyl 131	. . . . . . 7 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> -. (A \ (/)) e. Fin)
9	8	intnand 757	. . . . . 6 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> -. ((/) C_ X /\ (A \ (/)) e. Fin))
10		0ex 3446	. . . . . . . 8 |- (/) e. _V
11		sseq1 2637	. . . . . . . . 9 |- (x = (/) -> (x C_ X <-> (/) C_ X))
12		difeq2 2719	. . . . . . . . . 10 |- (x = (/) -> (A \ x) = (A \ (/)))
13	12	eleq1d 1963	. . . . . . . . 9 |- (x = (/) -> ((A \ x) e. Fin <-> (A \ (/)) e. Fin))
14	11, 13	anbi12d 690	. . . . . . . 8 |- (x = (/) -> ((x C_ X /\ (A \ x) e. Fin) <-> ((/) C_ X /\ (A \ (/)) e. Fin)))
15	10, 14	elab 2403	. . . . . . 7 |- ((/) e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> ((/) C_ X /\ (A \ (/)) e. Fin))
16	15	notbii 204	. . . . . 6 |- (-. (/) e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> -. ((/) C_ X /\ (A \ (/)) e. Fin))
17	9, 16	sylibr 217	. . . . 5 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> -. (/) e. {x | (x C_ X /\ (A \ x) e. Fin)})
18		simpl 346	. . . . . . . . . . 11 |- ((y C_ X /\ (A \ y) e. Fin) -> y C_ X)
19	18	a1i 8	. . . . . . . . . 10 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> ((y C_ X /\ (A \ y) e. Fin) -> y C_ X))
20		visset 2295	. . . . . . . . . . 11 |- y e. _V
21		sseq1 2637	. . . . . . . . . . . 12 |- (x = y -> (x C_ X <-> y C_ X))
22		difeq2 2719	. . . . . . . . . . . . 13 |- (x = y -> (A \ x) = (A \ y))
23	22	eleq1d 1963	. . . . . . . . . . . 12 |- (x = y -> ((A \ x) e. Fin <-> (A \ y) e. Fin))
24	21, 23	anbi12d 690	. . . . . . . . . . 11 |- (x = y -> ((x C_ X /\ (A \ x) e. Fin) <-> (y C_ X /\ (A \ y) e. Fin)))
25	20, 24	elab 2403	. . . . . . . . . 10 |- (y e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> (y C_ X /\ (A \ y) e. Fin))
26	19, 25	syl5ib 223	. . . . . . . . 9 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (y e. {x | (x C_ X /\ (A \ x) e. Fin)} -> y C_ X))
27	26	r19.21aiv 2175	. . . . . . . 8 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> A.y e. {x | (x C_ X /\ (A \ x) e. Fin)}y C_ X)
28		unissb 3208	. . . . . . . 8 |- (U.{x | (x C_ X /\ (A \ x) e. Fin)} C_ X <-> A.y e. {x | (x C_ X /\ (A \ x) e. Fin)}y C_ X)
29	27, 28	sylibr 217	. . . . . . 7 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> U.{x | (x C_ X /\ (A \ x) e. Fin)} C_ X)
30		ssdif0 2934	. . . . . . . . . . . . 13 |- (A C_ X <-> (A \ X) = (/))
31	30	biimpi 168	. . . . . . . . . . . 12 |- (A C_ X -> (A \ X) = (/))
32		emfin 10165	. . . . . . . . . . . 12 |- (/) e. Fin
33	31, 32	syl6eqel 1979	. . . . . . . . . . 11 |- (A C_ X -> (A \ X) e. Fin)
34	33	3ad2ant2 898	. . . . . . . . . 10 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (A \ X) e. Fin)
35		ssid 2634	. . . . . . . . . 10 |- X C_ X
36	34, 35	jctil 316	. . . . . . . . 9 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (X C_ X /\ (A \ X) e. Fin))
37		difeq2 2719	. . . . . . . . . . . 12 |- (x = X -> (A \ x) = (A \ X))
38	37	eleq1d 1963	. . . . . . . . . . 11 |- (x = X -> ((A \ x) e. Fin <-> (A \ X) e. Fin))
39	38	elssabg 3462	. . . . . . . . . 10 |- (X e. B -> (X e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> (X C_ X /\ (A \ X) e. Fin)))
40	39	3ad2ant1 897	. . . . . . . . 9 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (X e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> (X C_ X /\ (A \ X) e. Fin)))
41	36, 40	mpbird 213	. . . . . . . 8 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> X e. {x | (x C_ X /\ (A \ x) e. Fin)})
42		elssuni 3206	. . . . . . . 8 |- (X e. {x | (x C_ X /\ (A \ x) e. Fin)} -> X C_ U.{x | (x C_ X /\ (A \ x) e. Fin)})
43	41, 42	syl 12	. . . . . . 7 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> X C_ U.{x | (x C_ X /\ (A \ x) e. Fin)})
44	29, 43	eqssd 2633	. . . . . 6 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> U.{x | (x C_ X /\ (A \ x) e. Fin)} = X)
45	44, 41	eqeltrd 1971	. . . . 5 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> U.{x | (x C_ X /\ (A \ x) e. Fin)} e. {x | (x C_ X /\ (A \ x) e. Fin)})
46	17, 45	jca 310	. . . 4 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (-. (/) e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ U.{x | (x C_ X /\ (A \ x) e. Fin)} e. {x | (x C_ X /\ (A \ x) e. Fin)}))
47	44	sseq2d 2645	. . . . . . . . . 10 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (v C_ U.{x | (x C_ X /\ (A \ x) e. Fin)} <-> v C_ X))
48		simprl 450	. . . . . . . . . . . 12 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ (v C_ X /\ ((u C_ X /\ (A \ u) e. Fin) /\ u C_ v))) -> v C_ X)
49		simplr 449	. . . . . . . . . . . . . 14 |- (((u C_ X /\ (A \ u) e. Fin) /\ u C_ v) -> (A \ u) e. Fin)
50	49	ad2antll 443	. . . . . . . . . . . . 13 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ (v C_ X /\ ((u C_ X /\ (A \ u) e. Fin) /\ u C_ v))) -> (A \ u) e. Fin)
51		sscon 2739	. . . . . . . . . . . . . . 15 |- (u C_ v -> (A \ v) C_ (A \ u))
52	51	adantl 424	. . . . . . . . . . . . . 14 |- (((u C_ X /\ (A \ u) e. Fin) /\ u C_ v) -> (A \ v) C_ (A \ u))
53	52	ad2antll 443	. . . . . . . . . . . . 13 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ (v C_ X /\ ((u C_ X /\ (A \ u) e. Fin) /\ u C_ v))) -> (A \ v) C_ (A \ u))
54		ssfi 5630	. . . . . . . . . . . . 13 |- (((A \ u) e. Fin /\ (A \ v) C_ (A \ u)) -> (A \ v) e. Fin)
55	50, 53, 54	syl11anc 524	. . . . . . . . . . . 12 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ (v C_ X /\ ((u C_ X /\ (A \ u) e. Fin) /\ u C_ v))) -> (A \ v) e. Fin)
56	48, 55	jca 310	. . . . . . . . . . 11 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ (v C_ X /\ ((u C_ X /\ (A \ u) e. Fin) /\ u C_ v))) -> (v C_ X /\ (A \ v) e. Fin))
57	56	exp45 417	. . . . . . . . . 10 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (v C_ X -> ((u C_ X /\ (A \ u) e. Fin) -> (u C_ v -> (v C_ X /\ (A \ v) e. Fin)))))
58	47, 57	sylbid 220	. . . . . . . . 9 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (v C_ U.{x | (x C_ X /\ (A \ x) e. Fin)} -> ((u C_ X /\ (A \ u) e. Fin) -> (u C_ v -> (v C_ X /\ (A \ v) e. Fin)))))
59	58	com23 36	. . . . . . . 8 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> ((u C_ X /\ (A \ u) e. Fin) -> (v C_ U.{x | (x C_ X /\ (A \ x) e. Fin)} -> (u C_ v -> (v C_ X /\ (A \ v) e. Fin)))))
60		visset 2295	. . . . . . . . 9 |- u e. _V
61		sseq1 2637	. . . . . . . . . 10 |- (x = u -> (x C_ X <-> u C_ X))
62		difeq2 2719	. . . . . . . . . . 11 |- (x = u -> (A \ x) = (A \ u))
63	62	eleq1d 1963	. . . . . . . . . 10 |- (x = u -> ((A \ x) e. Fin <-> (A \ u) e. Fin))
64	61, 63	anbi12d 690	. . . . . . . . 9 |- (x = u -> ((x C_ X /\ (A \ x) e. Fin) <-> (u C_ X /\ (A \ u) e. Fin)))
65	60, 64	elab 2403	. . . . . . . 8 |- (u e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> (u C_ X /\ (A \ u) e. Fin))
66	59, 65	syl5ib 223	. . . . . . 7 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (u e. {x | (x C_ X /\ (A \ x) e. Fin)} -> (v C_ U.{x | (x C_ X /\ (A \ x) e. Fin)} -> (u C_ v -> (v C_ X /\ (A \ v) e. Fin)))))
67	66	3impd 1082	. . . . . 6 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> ((u e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ v C_ U.{x | (x C_ X /\ (A \ x) e. Fin)} /\ u C_ v) -> (v C_ X /\ (A \ v) e. Fin)))
68		visset 2295	. . . . . . 7 |- v e. _V
69		sseq1 2637	. . . . . . . 8 |- (x = v -> (x C_ X <-> v C_ X))
70		difeq2 2719	. . . . . . . . 9 |- (x = v -> (A \ x) = (A \ v))
71	70	eleq1d 1963	. . . . . . . 8 |- (x = v -> ((A \ x) e. Fin <-> (A \ v) e. Fin))
72	69, 71	anbi12d 690	. . . . . . 7 |- (x = v -> ((x C_ X /\ (A \ x) e. Fin) <-> (v C_ X /\ (A \ v) e. Fin)))
73	68, 72	elab 2403	. . . . . 6 |- (v e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> (v C_ X /\ (A \ v) e. Fin))
74	67, 73	syl6ibr 230	. . . . 5 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> ((u e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ v C_ U.{x | (x C_ X /\ (A \ x) e. Fin)} /\ u C_ v) -> v e. {x | (x C_ X /\ (A \ x) e. Fin)}))
75	74	19.21aivv 1665	. . . 4 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> A.uA.v((u e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ v C_ U.{x | (x C_ X /\ (A \ x) e. Fin)} /\ u C_ v) -> v e. {x | (x C_ X /\ (A \ x) e. Fin)}))
76		ssinss1 2821	. . . . . . . . 9 |- (u C_ X -> (u i^i v) C_ X)
77	76	ad2antrr 440	. . . . . . . 8 |- (((u C_ X /\ (A \ u) e. Fin) /\ (v C_ X /\ (A \ v) e. Fin)) -> (u i^i v) C_ X)
78		unfi 5644	. . . . . . . . . 10 |- (((A \ u) e. Fin /\ (A \ v) e. Fin) -> ((A \ u) u. (A \ v)) e. Fin)
79		difindi 2849	. . . . . . . . . 10 |- (A \ (u i^i v)) = ((A \ u) u. (A \ v))
80	78, 79	syl5eqel 1975	. . . . . . . . 9 |- (((A \ u) e. Fin /\ (A \ v) e. Fin) -> (A \ (u i^i v)) e. Fin)
81	80	ad2ant2l 444	. . . . . . . 8 |- (((u C_ X /\ (A \ u) e. Fin) /\ (v C_ X /\ (A \ v) e. Fin)) -> (A \ (u i^i v)) e. Fin)
82	77, 81	jca 310	. . . . . . 7 |- (((u C_ X /\ (A \ u) e. Fin) /\ (v C_ X /\ (A \ v) e. Fin)) -> ((u i^i v) C_ X /\ (A \ (u i^i v)) e. Fin))
83	82	a1i 8	. . . . . 6 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (((u C_ X /\ (A \ u) e. Fin) /\ (v C_ X /\ (A \ v) e. Fin)) -> ((u i^i v) C_ X /\ (A \ (u i^i v)) e. Fin)))
84	65, 73	anbi12i 540	. . . . . 6 |- ((u e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ v e. {x | (x C_ X /\ (A \ x) e. Fin)}) <-> ((u C_ X /\ (A \ u) e. Fin) /\ (v C_ X /\ (A \ v) e. Fin)))
85	60	inex1 3452	. . . . . . 7 |- (u i^i v) e. _V
86		sseq1 2637	. . . . . . . 8 |- (x = (u i^i v) -> (x C_ X <-> (u i^i v) C_ X))
87		difeq2 2719	. . . . . . . . 9 |- (x = (u i^i v) -> (A \ x) = (A \ (u i^i v)))
88	87	eleq1d 1963	. . . . . . . 8 |- (x = (u i^i v) -> ((A \ x) e. Fin <-> (A \ (u i^i v)) e. Fin))
89	86, 88	anbi12d 690	. . . . . . 7 |- (x = (u i^i v) -> ((x C_ X /\ (A \ x) e. Fin) <-> ((u i^i v) C_ X /\ (A \ (u i^i v)) e. Fin)))
90	85, 89	elab 2403	. . . . . 6 |- ((u i^i v) e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> ((u i^i v) C_ X /\ (A \ (u i^i v)) e. Fin))
91	83, 84, 90	3imtr4g 612	. . . . 5 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> ((u e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ v e. {x | (x C_ X /\ (A \ x) e. Fin)}) -> (u i^i v) e. {x | (x C_ X /\ (A \ x) e. Fin)}))
92	91	r19.21aivv 2183	. . . 4 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> A.u e. {x | (x C_ X /\ (A \ x) e. Fin)}A.v e. {x | (x C_ X /\ (A \ x) e. Fin)} (u i^i v) e. {x | (x C_ X /\ (A \ x) e. Fin)})
93	46, 75, 92	3jca 1050	. . 3 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> ((-. (/) e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ U.{x | (x C_ X /\ (A \ x) e. Fin)} e. {x | (x C_ X /\ (A \ x) e. Fin)}) /\ A.uA.v((u e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ v C_ U.{x | (x C_ X /\ (A \ x) e. Fin)} /\ u C_ v) -> v e. {x | (x C_ X /\ (A \ x) e. Fin)}) /\ A.u e. {x | (x C_ X /\ (A \ x) e. Fin)}A.v e. {x | (x C_ X /\ (A \ x) e. Fin)} (u i^i v) e. {x | (x C_ X /\ (A \ x) e. Fin)}))
94		abssexg 3490	. . . . 5 |- (X e. B -> {x | (x C_ X /\ (A \ x) e. Fin)} e. _V)
95		eqid 1884	. . . . . 6 |- U.{x | (x C_ X /\ (A \ x) e. Fin)} = U.{x | (x C_ X /\ (A \ x) e. Fin)}
96	95	isfil 10266	. . . . 5 |- ({x | (x C_ X /\ (A \ x) e. Fin)} e. _V -> ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil <-> ((-. (/) e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ U.{x | (x C_ X /\ (A \ x) e. Fin)} e. {x | (x C_ X /\ (A \ x) e. Fin)}) /\ A.uA.v((u e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ v C_ U.{x | (x C_ X /\ (A \ x) e. Fin)} /\ u C_ v) -> v e. {x | (x C_ X /\ (A \ x) e. Fin)}) /\ A.u e. {x | (x C_ X /\ (A \ x) e. Fin)}A.v e. {x | (x C_ X /\ (A \ x) e. Fin)} (u i^i v) e. {x | (x C_ X /\ (A \ x) e. Fin)})))
97	94, 96	syl 12	. . . 4 |- (X e. B -> ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil <-> ((-. (/) e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ U.{x | (x C_ X /\ (A \ x) e. Fin)} e. {x | (x C_ X /\ (A \ x) e. Fin)}) /\ A.uA.v((u e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ v C_ U.{x | (x C_ X /\ (A \ x) e. Fin)} /\ u C_ v) -> v e. {x | (x C_ X /\ (A \ x) e. Fin)}) /\ A.u e. {x | (x C_ X /\ (A \ x) e. Fin)}A.v e. {x | (x C_ X /\ (A \ x) e. Fin)} (u i^i v) e. {x | (x C_ X /\ (A \ x) e. Fin)})))
98	97	3ad2ant1 897	. . 3 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil <-> ((-. (/) e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ U.{x | (x C_ X /\ (A \ x) e. Fin)} e. {x | (x C_ X /\ (A \ x) e. Fin)}) /\ A.uA.v((u e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ v C_ U.{x | (x C_ X /\ (A \ x) e. Fin)} /\ u C_ v) -> v e. {x | (x C_ X /\ (A \ x) e. Fin)}) /\ A.u e. {x | (x C_ X /\ (A \ x) e. Fin)}A.v e. {x | (x C_ X /\ (A \ x) e. Fin)} (u i^i v) e. {x | (x C_ X /\ (A \ x) e. Fin)})))
99	93, 98	mpbird 213	. 2 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> {x | (x C_ X /\ (A \ x) e. Fin)} e. Fil)
100	95	filssufil 15571	. . . . 5 |- ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil -> E.f e. UFil (U.{x | (x C_ X /\ (A \ x) e. Fin)} = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f))
101	100	adantl 424	. . . 4 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ {x | (x C_ X /\ (A \ x) e. Fin)} e. Fil) -> E.f e. UFil (U.{x | (x C_ X /\ (A \ x) e. Fin)} = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f))
102	44	eqeq1d 1892	. . . . . . 7 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (U.{x | (x C_ X /\ (A \ x) e. Fin)} = U.f <-> X = U.f))
103	102	anbi1d 679	. . . . . 6 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> ((U.{x | (x C_ X /\ (A \ x) e. Fin)} = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f) <-> (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)))
104	103	rexbidv 2124	. . . . 5 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (E.f e. UFil (U.{x | (x C_ X /\ (A \ x) e. Fin)} = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f) <-> E.f e. UFil (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)))
105	104	adantr 425	. . . 4 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ {x | (x C_ X /\ (A \ x) e. Fin)} e. Fil) -> (E.f e. UFil (U.{x | (x C_ X /\ (A \ x) e. Fin)} = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f) <-> E.f e. UFil (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)))
106	101, 105	mpbid 212	. . 3 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ {x | (x C_ X /\ (A \ x) e. Fin)} e. Fil) -> E.f e. UFil (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f))
107		simpl 346	. . . . . . 7 |- ((X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f) -> X = U.f)
108	107	a1i 8	. . . . . 6 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) -> ((X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f) -> X = U.f))
109		simprr 451	. . . . . . . 8 |- ((((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) /\ (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)) -> {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)
110		simpr 350	. . . . . . . . . . . 12 |- ((X e. B /\ A C_ X) -> A C_ X)
111		difid 2942	. . . . . . . . . . . . 13 |- (A \ A) = (/)
112	111, 32	eqeltri 1967	. . . . . . . . . . . 12 |- (A \ A) e. Fin
113	110, 112	jctir 317	. . . . . . . . . . 11 |- ((X e. B /\ A C_ X) -> (A C_ X /\ (A \ A) e. Fin))
114		ssexg 3457	. . . . . . . . . . . . 13 |- ((A C_ X /\ X e. B) -> A e. _V)
115	114	ancoms 484	. . . . . . . . . . . 12 |- ((X e. B /\ A C_ X) -> A e. _V)
116		sseq1 2637	. . . . . . . . . . . . . 14 |- (x = A -> (x C_ X <-> A C_ X))
117		difeq2 2719	. . . . . . . . . . . . . . 15 |- (x = A -> (A \ x) = (A \ A))
118	117	eleq1d 1963	. . . . . . . . . . . . . 14 |- (x = A -> ((A \ x) e. Fin <-> (A \ A) e. Fin))
119	116, 118	anbi12d 690	. . . . . . . . . . . . 13 |- (x = A -> ((x C_ X /\ (A \ x) e. Fin) <-> (A C_ X /\ (A \ A) e. Fin)))
120	119	elabg 2405	. . . . . . . . . . . 12 |- (A e. _V -> (A e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> (A C_ X /\ (A \ A) e. Fin)))
121	115, 120	syl 12	. . . . . . . . . . 11 |- ((X e. B /\ A C_ X) -> (A e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> (A C_ X /\ (A \ A) e. Fin)))
122	113, 121	mpbird 213	. . . . . . . . . 10 |- ((X e. B /\ A C_ X) -> A e. {x | (x C_ X /\ (A \ x) e. Fin)})
123	122	3adant3 896	. . . . . . . . 9 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> A e. {x | (x C_ X /\ (A \ x) e. Fin)})
124	123	ad2antrr 440	. . . . . . . 8 |- ((((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) /\ (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)) -> A e. {x | (x C_ X /\ (A \ x) e. Fin)})
125	109, 124	sseldd 2620	. . . . . . 7 |- ((((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) /\ (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)) -> A e. f)
126	125	ex 402	. . . . . 6 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) -> ((X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f) -> A e. f))
127		intss 3239	. . . . . . . . . 10 |- ({x | (x C_ X /\ (A \ x) e. Fin)} C_ f -> |^|f C_ |^|{x | (x C_ X /\ (A \ x) e. Fin)})
128	127	ad2antll 443	. . . . . . . . 9 |- ((((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) /\ (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)) -> |^|f C_ |^|{x | (x C_ X /\ (A \ x) e. Fin)})
129		difexg 3458	. . . . . . . . . . . . . . . 16 |- (A e. _V -> (A \ {y}) e. _V)
130	115, 129	syl 12	. . . . . . . . . . . . . . 15 |- ((X e. B /\ A C_ X) -> (A \ {y}) e. _V)
131	130	3adant3 896	. . . . . . . . . . . . . 14 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (A \ {y}) e. _V)
132		ssdifss 2736	. . . . . . . . . . . . . . . . . 18 |- (A C_ X -> (A \ {y}) C_ X)
133	132	3ad2ant2 898	. . . . . . . . . . . . . . . . 17 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (A \ {y}) C_ X)
134		snfi 5491	. . . . . . . . . . . . . . . . . 18 |- {y} e. Fin
135		eldif 2609	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. (A \ (A \ {y})) <-> (x e. A /\ -. x e. (A \ {y})))
136		eldif 2609	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. (A \ {y}) <-> (x e. A /\ -. x e. {y}))
137	136	notbii 204	. . . . . . . . . . . . . . . . . . . . . . 23 |- (-. x e. (A \ {y}) <-> -. (x e. A /\ -. x e. {y}))
138		iman 256	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. A -> x e. {y}) <-> -. (x e. A /\ -. x e. {y}))
139	137, 138	bitr4i 193	. . . . . . . . . . . . . . . . . . . . . 22 |- (-. x e. (A \ {y}) <-> (x e. A -> x e. {y}))
140	139	anbi2i 538	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. A /\ -. x e. (A \ {y})) <-> (x e. A /\ (x e. A -> x e. {y})))
141	135, 140	bitri 190	. . . . . . . . . . . . . . . . . . . 20 |- (x e. (A \ (A \ {y})) <-> (x e. A /\ (x e. A -> x e. {y})))
142		pm3.35 386	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. A /\ (x e. A -> x e. {y})) -> x e. {y})
143	141, 142	sylbi 216	. . . . . . . . . . . . . . . . . . 19 |- (x e. (A \ (A \ {y})) -> x e. {y})
144	143	ssriv 2621	. . . . . . . . . . . . . . . . . 18 |- (A \ (A \ {y})) C_ {y}
145		ssfi 5630	. . . . . . . . . . . . . . . . . 18 |- (({y} e. Fin /\ (A \ (A \ {y})) C_ {y}) -> (A \ (A \ {y})) e. Fin)
146	134, 144, 145	mp2an 761	. . . . . . . . . . . . . . . . 17 |- (A \ (A \ {y})) e. Fin
147	133, 146	jctir 317	. . . . . . . . . . . . . . . 16 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> ((A \ {y}) C_ X /\ (A \ (A \ {y})) e. Fin))
148		sseq1 2637	. . . . . . . . . . . . . . . . . . . 20 |- (x = (A \ {y}) -> (x C_ X <-> (A \ {y}) C_ X))
149		difeq2 2719	. . . . . . . . . . . . . . . . . . . . 21 |- (x = (A \ {y}) -> (A \ x) = (A \ (A \ {y})))
150	149	eleq1d 1963	. . . . . . . . . . . . . . . . . . . 20 |- (x = (A \ {y}) -> ((A \ x) e. Fin <-> (A \ (A \ {y})) e. Fin))
151	148, 150	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- (x = (A \ {y}) -> ((x C_ X /\ (A \ x) e. Fin) <-> ((A \ {y}) C_ X /\ (A \ (A \ {y})) e. Fin)))
152	151	elabg 2405	. . . . . . . . . . . . . . . . . 18 |- ((A \ {y}) e. _V -> ((A \ {y}) e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> ((A \ {y}) C_ X /\ (A \ (A \ {y})) e. Fin)))
153	115, 129, 152	3syl 24	. . . . . . . . . . . . . . . . 17 |- ((X e. B /\ A C_ X) -> ((A \ {y}) e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> ((A \ {y}) C_ X /\ (A \ (A \ {y})) e. Fin)))
154	153	3adant3 896	. . . . . . . . . . . . . . . 16 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> ((A \ {y}) e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> ((A \ {y}) C_ X /\ (A \ (A \ {y})) e. Fin)))
155	147, 154	mpbird 213	. . . . . . . . . . . . . . 15 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> (A \ {y}) e. {x | (x C_ X /\ (A \ x) e. Fin)})
156	20	snid 3069	. . . . . . . . . . . . . . . 16 |- y e. {y}
157		elndif 2732	. . . . . . . . . . . . . . . 16 |- (y e. {y} -> -. y e. (A \ {y}))
158	156, 157	ax-mp 7	. . . . . . . . . . . . . . 15 |- -. y e. (A \ {y})
159	155, 158	jctir 317	. . . . . . . . . . . . . 14 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> ((A \ {y}) e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ -. y e. (A \ {y})))
160		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (z = (A \ {y}) -> (z e. {x | (x C_ X /\ (A \ x) e. Fin)} <-> (A \ {y}) e. {x | (x C_ X /\ (A \ x) e. Fin)}))
161		eleq2 1958	. . . . . . . . . . . . . . . . 17 |- (z = (A \ {y}) -> (y e. z <-> y e. (A \ {y})))
162	161	notbid 673	. . . . . . . . . . . . . . . 16 |- (z = (A \ {y}) -> (-. y e. z <-> -. y e. (A \ {y})))
163	160, 162	anbi12d 690	. . . . . . . . . . . . . . 15 |- (z = (A \ {y}) -> ((z e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ -. y e. z) <-> ((A \ {y}) e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ -. y e. (A \ {y}))))
164	163	cla4egv 2365	. . . . . . . . . . . . . 14 |- ((A \ {y}) e. _V -> (((A \ {y}) e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ -. y e. (A \ {y})) -> E.z(z e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ -. y e. z)))
165	131, 159, 164	sylc 83	. . . . . . . . . . . . 13 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> E.z(z e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ -. y e. z))
166	165	ad2antrr 440	. . . . . . . . . . . 12 |- ((((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) /\ (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)) -> E.z(z e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ -. y e. z))
167		exanali 1390	. . . . . . . . . . . . 13 |- (E.z(z e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ -. y e. z) <-> -. A.z(z e. {x | (x C_ X /\ (A \ x) e. Fin)} -> y e. z))
168	20	elint 3220	. . . . . . . . . . . . . 14 |- (y e. |^|{x | (x C_ X /\ (A \ x) e. Fin)} <-> A.z(z e. {x | (x C_ X /\ (A \ x) e. Fin)} -> y e. z))
169	168	notbii 204	. . . . . . . . . . . . 13 |- (-. y e. |^|{x | (x C_ X /\ (A \ x) e. Fin)} <-> -. A.z(z e. {x | (x C_ X /\ (A \ x) e. Fin)} -> y e. z))
170	167, 169	bitr4i 193	. . . . . . . . . . . 12 |- (E.z(z e. {x | (x C_ X /\ (A \ x) e. Fin)} /\ -. y e. z) <-> -. y e. |^|{x | (x C_ X /\ (A \ x) e. Fin)})
171	166, 170	sylib 215	. . . . . . . . . . 11 |- ((((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) /\ (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)) -> -. y e. |^|{x | (x C_ X /\ (A \ x) e. Fin)})
172	171	19.21aiv 1664	. . . . . . . . . 10 |- ((((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) /\ (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)) -> A.y -. y e. |^|{x | (x C_ X /\ (A \ x) e. Fin)})
173		eq0 2889	. . . . . . . . . 10 |- (|^|{x | (x C_ X /\ (A \ x) e. Fin)} = (/) <-> A.y -. y e. |^|{x | (x C_ X /\ (A \ x) e. Fin)})
174	172, 173	sylibr 217	. . . . . . . . 9 |- ((((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) /\ (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)) -> |^|{x | (x C_ X /\ (A \ x) e. Fin)} = (/))
175	128, 174	sseqtrd 2653	. . . . . . . 8 |- ((((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) /\ (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f)) -> |^|f C_ (/))
176	175	ex 402	. . . . . . 7 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) -> ((X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f) -> |^|f C_ (/)))
177		ss0 2902	. . . . . . 7 |- (|^|f C_ (/) -> |^|f = (/))
178	176, 177	syl6 25	. . . . . 6 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) -> ((X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f) -> |^|f = (/)))
179	108, 126, 178	3jcad 1051	. . . . 5 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ ({x | (x C_ X /\ (A \ x) e. Fin)} e. Fil /\ f e. UFil)) -> ((X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f) -> (X = U.f /\ A e. f /\ |^|f = (/))))
180	179	expr 418	. . . 4 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ {x | (x C_ X /\ (A \ x) e. Fin)} e. Fil) -> (f e. UFil -> ((X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f) -> (X = U.f /\ A e. f /\ |^|f = (/)))))
181	180	reximdvai 2201	. . 3 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ {x | (x C_ X /\ (A \ x) e. Fin)} e. Fil) -> (E.f e. UFil (X = U.f /\ {x | (x C_ X /\ (A \ x) e. Fin)} C_ f) -> E.f e. UFil (X = U.f /\ A e. f /\ |^|f = (/))))
182	106, 181	mpd 29	. 2 |- (((X e. B /\ A C_ X /\ om ~<_ A) /\ {x | (x C_ X /\ (A \ x) e. Fin)} e. Fil) -> E.f e. UFil (X = U.f /\ A e. f /\ |^|f = (/)))
183	99, 182	mpdan 768	1 |- ((X e. B /\ A C_ X /\ om ~<_ A) -> E.f e. UFil (X = U.f /\ A e. f /\ |^|f = (/)))

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  A.wral 2105  E.wrex 2106  _Vcvv 2292   \ cdif 2590   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177  |^|cint 3214   class class class wbr 3338  omcom 3949   ~<_ cdom 5424   ~< csdm 5425  Fincfn 5426  Filcfil 10264  UFilcufil 15562

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  ax-inf2 5731  ax-ac 5906

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-iso 4015  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429  df-fin 5430  df-fi 10211  df-fbas 10259  df-fg 10260  df-fil 10265  df-ufil 15563

Copyright terms: Public domain