MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dffi3 Unicode version

Theorem dffi3 7911
Description: The set of finite intersections can be "constructed" inductively by iterating binary intersection -many times. (Contributed by Mario Carneiro, 21-Mar-2015.)
Hypothesis
Ref Expression
dffi3.1
Assertion
Ref Expression
dffi3
Distinct variable groups:   ,   ,   ,   , ,

Proof of Theorem dffi3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dffi2 7903 . . . 4
2 fr0g 7120 . . . . . . . 8
3 frfnom 7119 . . . . . . . . 9
4 peano1 6719 . . . . . . . . 9
5 fnfvelrn 6028 . . . . . . . . 9
63, 4, 5mp2an 672 . . . . . . . 8
72, 6syl6eqelr 2554 . . . . . . 7
8 elssuni 4279 . . . . . . 7
97, 8syl 16 . . . . . 6
10 reeanv 3025 . . . . . . . . 9
11 eliun 4335 . . . . . . . . . 10
12 eliun 4335 . . . . . . . . . 10
1311, 12anbi12i 697 . . . . . . . . 9
14 fniunfv 6159 . . . . . . . . . . . 12
1514eleq2d 2527 . . . . . . . . . . 11
16 fniunfv 6159 . . . . . . . . . . . 12
1716eleq2d 2527 . . . . . . . . . . 11
1815, 17anbi12d 710 . . . . . . . . . 10
193, 18ax-mp 5 . . . . . . . . 9
2010, 13, 193bitr2i 273 . . . . . . . 8
21 ordom 6709 . . . . . . . . . . . . . . . 16
22 ordunel 6662 . . . . . . . . . . . . . . . 16
2321, 22mp3an1 1311 . . . . . . . . . . . . . . 15
2423adantl 466 . . . . . . . . . . . . . 14
25 simprl 756 . . . . . . . . . . . . . 14
2624, 25jca 532 . . . . . . . . . . . . 13
27 nnon 6706 . . . . . . . . . . . . . . . . . . 19
2827adantl 466 . . . . . . . . . . . . . . . . . 18
29 nnon 6706 . . . . . . . . . . . . . . . . . . 19
3029ad2antlr 726 . . . . . . . . . . . . . . . . . 18
31 onsseleq 4924 . . . . . . . . . . . . . . . . . 18
3228, 30, 31syl2anc 661 . . . . . . . . . . . . . . . . 17
33 rzal 3931 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3433biantrud 507 . . . . . . . . . . . . . . . . . . . . . . . . 25
35 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3635sseq1d 3530 . . . . . . . . . . . . . . . . . . . . . . . . 25
3734, 36bitr3d 255 . . . . . . . . . . . . . . . . . . . . . . . 24
38 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3938sseq1d 3530 . . . . . . . . . . . . . . . . . . . . . . . . 25
4038sseq2d 3531 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4140raleqbi1dv 3062 . . . . . . . . . . . . . . . . . . . . . . . . 25
4239, 41anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . 24
43 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4443sseq1d 3530 . . . . . . . . . . . . . . . . . . . . . . . . 25
4543sseq2d 3531 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4645raleqbi1dv 3062 . . . . . . . . . . . . . . . . . . . . . . . . 25
4744, 46anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . 24
48 ssfii 7899 . . . . . . . . . . . . . . . . . . . . . . . . 25
492, 48eqsstrd 3537 . . . . . . . . . . . . . . . . . . . . . . . 24
50 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51 eqidd 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
52 ineq1 3692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
5352eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54 ineq2 3693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55 inidm 3706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
5654, 55syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
5756eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
5853, 57rspc2ev 3221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5950, 50, 51, 58syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6160rnmpt2 6412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6261abeq2i 2584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6359, 62sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6463ssriv 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66 fvex 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6766uniex 6596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6867pwex 4635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
69 inss1 3717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
70 elssuni 4279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
7170adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
7269, 71syl5ss 3514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
73 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
7473inex1 4593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
7574elpw 4018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
7672, 75sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
7776rgen2a 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
7860fmpt2 6867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
7977, 78mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
80 frn 5742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
8179, 80ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
8268, 81ssexi 4597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83 nfcv 2619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84 nfcv 2619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85 nfcv 2619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
86 dffi3.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
87 mpt2eq12 6357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
8887anidms 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
89 ineq1 3692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
90 ineq2 3693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
9189, 90cbvmpt2v 6377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
9288, 91syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
9392rneqd 5235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
9493cbvmptv 4543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
9586, 94eqtri 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96 rdgeq1 7096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9897reseq1i 5274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99 mpt2eq12 6357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
10099anidms 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101100rneqd 5235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
10283, 84, 85, 98, 101frsucmpt 7122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
10365, 82, 102sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
10464, 103syl5sseqr 3552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
105 sstr2 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106104, 105syl5com 30 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
107106ralimdv 2867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110109sseq1d 3530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111108, 110ralsn 4068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112104, 111sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
113107, 112jctird 544 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
114 df-suc 4889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115114raleqi 3058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116 ralunb 3684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
117115, 116bitri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
118113, 117syl6ibr 227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
119 fiin 7902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
120119rgen2a 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121 ssralv 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122121ralimdv 2867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123 ssralv 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124122, 123syld 44 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125120, 124mpi 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
12660fmpt2 6867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127125, 126sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128 frn 5742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129127, 128syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130129adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
131103, 130eqsstrd 3537 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 </