Theorem trufil 20389

Description: Conditions for the trace of an ultrafilter L to be an ultrafilter. (Contributed by Mario Carneiro, 27-Aug-2015.)

Assertion

Ref	Expression
trufil	|- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( ( L ↾t A ) e. ( UFil ` A ) <-> A e. L ) )

Proof of Theorem trufil

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ufilfil 20383	. . . 4 |- ( ( L ↾t A ) e. ( UFil ` A ) -> ( L ↾t A ) e. ( Fil ` A ) )
2		ufilfil 20383	. . . . 5 |- ( L e. ( UFil ` Y ) -> L e. ( Fil ` Y ) )
3		trfil3 20367	. . . . 5 |- ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( L ↾t A ) e. ( Fil ` A ) <-> -. ( Y \ A ) e. L ) )
4	2, 3	sylan 471	. . . 4 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( ( L ↾t A ) e. ( Fil ` A ) <-> -. ( Y \ A ) e. L ) )
5	1, 4	syl5ib 219	. . 3 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( ( L ↾t A ) e. ( UFil ` A ) -> -. ( Y \ A ) e. L ) )
6	4	biimprd 223	. . . . 5 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( -. ( Y \ A ) e. L -> ( L ↾t A ) e. ( Fil ` A ) ) )
7		elpwi 4006	. . . . . . 7 |- ( x e. ~P A -> x C_ A )
8		simpll 753	. . . . . . . . 9 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> L e. ( UFil ` Y ) )
9		simpr 461	. . . . . . . . . 10 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> x C_ A )
10		simplr 755	. . . . . . . . . 10 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> A C_ Y )
11	9, 10	sstrd 3499	. . . . . . . . 9 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> x C_ Y )
12		ufilss 20384	. . . . . . . . 9 |- ( ( L e. ( UFil ` Y ) /\ x C_ Y ) -> ( x e. L \/ ( Y \ x ) e. L ) )
13	8, 11, 12	syl2anc 661	. . . . . . . 8 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( x e. L \/ ( Y \ x ) e. L ) )
14		id 22	. . . . . . . . . . . . 13 |- ( A C_ Y -> A C_ Y )
15		elfvdm 5882	. . . . . . . . . . . . 13 |- ( L e. ( UFil ` Y ) -> Y e. dom UFil )
16		ssexg 4583	. . . . . . . . . . . . 13 |- ( ( A C_ Y /\ Y e. dom UFil ) -> A e. _V )
17	14, 15, 16	syl2anr 478	. . . . . . . . . . . 12 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> A e. _V )
18		elrestr 14808	. . . . . . . . . . . . 13 |- ( ( L e. ( UFil ` Y ) /\ A e. _V /\ x e. L ) -> ( x i^i A ) e. ( L ↾t A ) )
19	18	3expia 1199	. . . . . . . . . . . 12 |- ( ( L e. ( UFil ` Y ) /\ A e. _V ) -> ( x e. L -> ( x i^i A ) e. ( L ↾t A ) ) )
20	17, 19	syldan 470	. . . . . . . . . . 11 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( x e. L -> ( x i^i A ) e. ( L ↾t A ) ) )
21	20	adantr 465	. . . . . . . . . 10 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( x e. L -> ( x i^i A ) e. ( L ↾t A ) ) )
22		df-ss 3475	. . . . . . . . . . . 12 |- ( x C_ A <-> ( x i^i A ) = x )
23	9, 22	sylib 196	. . . . . . . . . . 11 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( x i^i A ) = x )
24	23	eleq1d 2512	. . . . . . . . . 10 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( ( x i^i A ) e. ( L ↾t A ) <-> x e. ( L ↾t A ) ) )
25	21, 24	sylibd 214	. . . . . . . . 9 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( x e. L -> x e. ( L ↾t A ) ) )
26		indif1 3727	. . . . . . . . . . . 12 |- ( ( Y \ x ) i^i A ) = ( ( Y i^i A ) \ x )
27		simplr 755	. . . . . . . . . . . . . 14 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> A C_ Y )
28		dfss1 3688	. . . . . . . . . . . . . 14 |- ( A C_ Y <-> ( Y i^i A ) = A )
29	27, 28	sylib 196	. . . . . . . . . . . . 13 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( Y i^i A ) = A )
30	29	difeq1d 3606	. . . . . . . . . . . 12 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( ( Y i^i A ) \ x ) = ( A \ x ) )
31	26, 30	syl5eq 2496	. . . . . . . . . . 11 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( ( Y \ x ) i^i A ) = ( A \ x ) )
32		simpll 753	. . . . . . . . . . . 12 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> L e. ( UFil ` Y ) )
33	17	adantr 465	. . . . . . . . . . . 12 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> A e. _V )
34		simprr 757	. . . . . . . . . . . 12 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( Y \ x ) e. L )
35		elrestr 14808	. . . . . . . . . . . 12 |- ( ( L e. ( UFil ` Y ) /\ A e. _V /\ ( Y \ x ) e. L ) -> ( ( Y \ x ) i^i A ) e. ( L ↾t A ) )
36	32, 33, 34, 35	syl3anc 1229	. . . . . . . . . . 11 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( ( Y \ x ) i^i A ) e. ( L ↾t A ) )
37	31, 36	eqeltrrd 2532	. . . . . . . . . 10 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( A \ x ) e. ( L ↾t A ) )
38	37	expr 615	. . . . . . . . 9 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( ( Y \ x ) e. L -> ( A \ x ) e. ( L ↾t A ) ) )
39	25, 38	orim12d 838	. . . . . . . 8 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( ( x e. L \/ ( Y \ x ) e. L ) -> ( x e. ( L ↾t A ) \/ ( A \ x ) e. ( L ↾t A ) ) ) )
40	13, 39	mpd 15	. . . . . . 7 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( x e. ( L ↾t A ) \/ ( A \ x ) e. ( L ↾t A ) ) )
41	7, 40	sylan2 474	. . . . . 6 |- ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x e. ~P A ) -> ( x e. ( L ↾t A ) \/ ( A \ x ) e. ( L ↾t A ) ) )
42	41	ralrimiva 2857	. . . . 5 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> A. x e. ~P A ( x e. ( L ↾t A ) \/ ( A \ x ) e. ( L ↾t A ) ) )
43	6, 42	jctird 544	. . . 4 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( -. ( Y \ A ) e. L -> ( ( L ↾t A ) e. ( Fil ` A ) /\ A. x e. ~P A ( x e. ( L ↾t A ) \/ ( A \ x ) e. ( L ↾t A ) ) ) ) )
44		isufil 20382	. . . 4 |- ( ( L ↾t A ) e. ( UFil ` A ) <-> ( ( L ↾t A ) e. ( Fil ` A ) /\ A. x e. ~P A ( x e. ( L ↾t A ) \/ ( A \ x ) e. ( L ↾t A ) ) ) )
45	43, 44	syl6ibr 227	. . 3 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( -. ( Y \ A ) e. L -> ( L ↾t A ) e. ( UFil ` A ) ) )
46	5, 45	impbid 191	. 2 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( ( L ↾t A ) e. ( UFil ` A ) <-> -. ( Y \ A ) e. L ) )
47		ufilb 20385	. . 3 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( -. A e. L <-> ( Y \ A ) e. L ) )
48	47	con1bid 330	. 2 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( -. ( Y \ A ) e. L <-> A e. L ) )
49	46, 48	bitrd 253	1 |- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( ( L ↾t A ) e. ( UFil ` A ) <-> A e. L ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1383   e. wcel 1804   A.wral 2793   _Vcvv 3095   \ cdif 3458   i^i cin 3460   C_ wss 3461   ~Pcpw 3997   dom cdm 4989   ` cfv 5578  (class class class)co 6281   ↾_t crest 14800   Filcfil 20324   UFilcufil 20378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-1st 6785  df-2nd 6786  df-rest 14802  df-fbas 18395  df-fg 18396  df-fil 20325  df-ufil 20380

This theorem is referenced by:  ssufl  20397