# Metamath Proof Explorer

## Theorem fiint

Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of A is in A ". This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002)

Ref Expression
Assertion fiint ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in {A}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)$

### Proof

Step Hyp Ref Expression
1 isfi ${⊢}{x}\in \mathrm{Fin}↔\exists {y}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}\approx {y}$
2 ensym ${⊢}{x}\approx {y}\to {y}\approx {x}$
3 breq1 ${⊢}{y}=\varnothing \to \left({y}\approx {x}↔\varnothing \approx {x}\right)$
4 3 anbi2d ${⊢}{y}=\varnothing \to \left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)↔\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \varnothing \approx {x}\right)\right)$
5 4 imbi1d ${⊢}{y}=\varnothing \to \left(\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)\to \bigcap {x}\in {A}\right)↔\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \varnothing \approx {x}\right)\to \bigcap {x}\in {A}\right)\right)$
6 5 albidv ${⊢}{y}=\varnothing \to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)\to \bigcap {x}\in {A}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \varnothing \approx {x}\right)\to \bigcap {x}\in {A}\right)\right)$
7 breq1 ${⊢}{y}={v}\to \left({y}\approx {x}↔{v}\approx {x}\right)$
8 7 anbi2d ${⊢}{y}={v}\to \left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)↔\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\right)$
9 8 imbi1d ${⊢}{y}={v}\to \left(\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)\to \bigcap {x}\in {A}\right)↔\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)$
10 9 albidv ${⊢}{y}={v}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)\to \bigcap {x}\in {A}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)$
11 breq1 ${⊢}{y}=\mathrm{suc}{v}\to \left({y}\approx {x}↔\mathrm{suc}{v}\approx {x}\right)$
12 11 anbi2d ${⊢}{y}=\mathrm{suc}{v}\to \left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)↔\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \mathrm{suc}{v}\approx {x}\right)\right)$
13 12 imbi1d ${⊢}{y}=\mathrm{suc}{v}\to \left(\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)\to \bigcap {x}\in {A}\right)↔\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \mathrm{suc}{v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)$
14 13 albidv ${⊢}{y}=\mathrm{suc}{v}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)\to \bigcap {x}\in {A}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \mathrm{suc}{v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)$
15 ensym ${⊢}\varnothing \approx {x}\to {x}\approx \varnothing$
16 en0 ${⊢}{x}\approx \varnothing ↔{x}=\varnothing$
17 15 16 sylib ${⊢}\varnothing \approx {x}\to {x}=\varnothing$
18 17 anim1i ${⊢}\left(\varnothing \approx {x}\wedge {x}\ne \varnothing \right)\to \left({x}=\varnothing \wedge {x}\ne \varnothing \right)$
19 18 ancoms ${⊢}\left({x}\ne \varnothing \wedge \varnothing \approx {x}\right)\to \left({x}=\varnothing \wedge {x}\ne \varnothing \right)$
20 19 adantll ${⊢}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \varnothing \approx {x}\right)\to \left({x}=\varnothing \wedge {x}\ne \varnothing \right)$
21 df-ne ${⊢}{x}\ne \varnothing ↔¬{x}=\varnothing$
22 pm3.24 ${⊢}¬\left({x}=\varnothing \wedge ¬{x}=\varnothing \right)$
23 22 pm2.21i ${⊢}\left({x}=\varnothing \wedge ¬{x}=\varnothing \right)\to \bigcap {x}\in {A}$
24 21 23 sylan2b ${⊢}\left({x}=\varnothing \wedge {x}\ne \varnothing \right)\to \bigcap {x}\in {A}$
25 20 24 syl ${⊢}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \varnothing \approx {x}\right)\to \bigcap {x}\in {A}$
26 25 ax-gen ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \varnothing \approx {x}\right)\to \bigcap {x}\in {A}\right)$
27 26 a1i ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \varnothing \approx {x}\right)\to \bigcap {x}\in {A}\right)$
28 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}$
29 nfa1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)$
30 bren ${⊢}\mathrm{suc}{v}\approx {x}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}$
31 ssel ${⊢}{x}\subseteq {A}\to \left({f}\left({v}\right)\in {x}\to {f}\left({v}\right)\in {A}\right)$
32 f1of ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {f}:\mathrm{suc}{v}⟶{x}$
33 vex ${⊢}{v}\in \mathrm{V}$
34 33 sucid ${⊢}{v}\in \mathrm{suc}{v}$
35 ffvelrn ${⊢}\left({f}:\mathrm{suc}{v}⟶{x}\wedge {v}\in \mathrm{suc}{v}\right)\to {f}\left({v}\right)\in {x}$
36 32 34 35 sylancl ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {f}\left({v}\right)\in {x}$
37 31 36 impel ${⊢}\left({x}\subseteq {A}\wedge {f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\right)\to {f}\left({v}\right)\in {A}$
38 37 adantr ${⊢}\left(\left({x}\subseteq {A}\wedge {f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\right)\right)\to {f}\left({v}\right)\in {A}$
39 df-ne ${⊢}{f}\left[{v}\right]\ne \varnothing ↔¬{f}\left[{v}\right]=\varnothing$
40 imassrn ${⊢}{f}\left[{v}\right]\subseteq \mathrm{ran}{f}$
41 dff1o2 ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}↔\left({f}Fn\mathrm{suc}{v}\wedge \mathrm{Fun}{{f}}^{-1}\wedge \mathrm{ran}{f}={x}\right)$
42 41 simp3bi ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \mathrm{ran}{f}={x}$
43 40 42 sseqtrid ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {f}\left[{v}\right]\subseteq {x}$
44 sstr2 ${⊢}{f}\left[{v}\right]\subseteq {x}\to \left({x}\subseteq {A}\to {f}\left[{v}\right]\subseteq {A}\right)$
45 43 44 syl ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \left({x}\subseteq {A}\to {f}\left[{v}\right]\subseteq {A}\right)$
46 45 anim1d ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \left(\left({x}\subseteq {A}\wedge {f}\left[{v}\right]\ne \varnothing \right)\to \left({f}\left[{v}\right]\subseteq {A}\wedge {f}\left[{v}\right]\ne \varnothing \right)\right)$
47 f1of1 ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {f}:\mathrm{suc}{v}\underset{1-1}{⟶}{x}$
48 vex ${⊢}{x}\in \mathrm{V}$
49 sssucid ${⊢}{v}\subseteq \mathrm{suc}{v}$
50 f1imaen2g ${⊢}\left(\left({f}:\mathrm{suc}{v}\underset{1-1}{⟶}{x}\wedge {x}\in \mathrm{V}\right)\wedge \left({v}\subseteq \mathrm{suc}{v}\wedge {v}\in \mathrm{V}\right)\right)\to {f}\left[{v}\right]\approx {v}$
51 49 33 50 mpanr12 ${⊢}\left({f}:\mathrm{suc}{v}\underset{1-1}{⟶}{x}\wedge {x}\in \mathrm{V}\right)\to {f}\left[{v}\right]\approx {v}$
52 47 48 51 sylancl ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {f}\left[{v}\right]\approx {v}$
53 52 ensymd ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {v}\approx {f}\left[{v}\right]$
54 46 53 jctird ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \left(\left({x}\subseteq {A}\wedge {f}\left[{v}\right]\ne \varnothing \right)\to \left(\left({f}\left[{v}\right]\subseteq {A}\wedge {f}\left[{v}\right]\ne \varnothing \right)\wedge {v}\approx {f}\left[{v}\right]\right)\right)$
55 vex ${⊢}{f}\in \mathrm{V}$
56 55 imaex ${⊢}{f}\left[{v}\right]\in \mathrm{V}$
57 sseq1 ${⊢}{x}={f}\left[{v}\right]\to \left({x}\subseteq {A}↔{f}\left[{v}\right]\subseteq {A}\right)$
58 neeq1 ${⊢}{x}={f}\left[{v}\right]\to \left({x}\ne \varnothing ↔{f}\left[{v}\right]\ne \varnothing \right)$
59 57 58 anbi12d ${⊢}{x}={f}\left[{v}\right]\to \left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)↔\left({f}\left[{v}\right]\subseteq {A}\wedge {f}\left[{v}\right]\ne \varnothing \right)\right)$
60 breq2 ${⊢}{x}={f}\left[{v}\right]\to \left({v}\approx {x}↔{v}\approx {f}\left[{v}\right]\right)$
61 59 60 anbi12d ${⊢}{x}={f}\left[{v}\right]\to \left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)↔\left(\left({f}\left[{v}\right]\subseteq {A}\wedge {f}\left[{v}\right]\ne \varnothing \right)\wedge {v}\approx {f}\left[{v}\right]\right)\right)$
62 inteq ${⊢}{x}={f}\left[{v}\right]\to \bigcap {x}=\bigcap {f}\left[{v}\right]$
63 62 eleq1d ${⊢}{x}={f}\left[{v}\right]\to \left(\bigcap {x}\in {A}↔\bigcap {f}\left[{v}\right]\in {A}\right)$
64 61 63 imbi12d ${⊢}{x}={f}\left[{v}\right]\to \left(\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)↔\left(\left(\left({f}\left[{v}\right]\subseteq {A}\wedge {f}\left[{v}\right]\ne \varnothing \right)\wedge {v}\approx {f}\left[{v}\right]\right)\to \bigcap {f}\left[{v}\right]\in {A}\right)\right)$
65 56 64 spcv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \left(\left(\left({f}\left[{v}\right]\subseteq {A}\wedge {f}\left[{v}\right]\ne \varnothing \right)\wedge {v}\approx {f}\left[{v}\right]\right)\to \bigcap {f}\left[{v}\right]\in {A}\right)$
66 54 65 sylan9 ${⊢}\left({f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)\to \left(\left({x}\subseteq {A}\wedge {f}\left[{v}\right]\ne \varnothing \right)\to \bigcap {f}\left[{v}\right]\in {A}\right)$
67 ineq1 ${⊢}{z}=\bigcap {f}\left[{v}\right]\to {z}\cap {w}=\bigcap {f}\left[{v}\right]\cap {w}$
68 67 eleq1d ${⊢}{z}=\bigcap {f}\left[{v}\right]\to \left({z}\cap {w}\in {A}↔\bigcap {f}\left[{v}\right]\cap {w}\in {A}\right)$
69 ineq2 ${⊢}{w}={f}\left({v}\right)\to \bigcap {f}\left[{v}\right]\cap {w}=\bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)$
70 69 eleq1d ${⊢}{w}={f}\left({v}\right)\to \left(\bigcap {f}\left[{v}\right]\cap {w}\in {A}↔\bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}\right)$
71 68 70 rspc2v ${⊢}\left(\bigcap {f}\left[{v}\right]\in {A}\wedge {f}\left({v}\right)\in {A}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}\right)$
72 71 ex ${⊢}\bigcap {f}\left[{v}\right]\in {A}\to \left({f}\left({v}\right)\in {A}\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}\right)\right)$
73 66 72 syl6 ${⊢}\left({f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)\to \left(\left({x}\subseteq {A}\wedge {f}\left[{v}\right]\ne \varnothing \right)\to \left({f}\left({v}\right)\in {A}\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}\right)\right)\right)$
74 73 com4r ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \left(\left({f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)\to \left(\left({x}\subseteq {A}\wedge {f}\left[{v}\right]\ne \varnothing \right)\to \left({f}\left({v}\right)\in {A}\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}\right)\right)\right)$
75 74 exp5c ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \left({f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \left({x}\subseteq {A}\to \left({f}\left[{v}\right]\ne \varnothing \to \left({f}\left({v}\right)\in {A}\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}\right)\right)\right)\right)\right)$
76 75 com14 ${⊢}{x}\subseteq {A}\to \left({f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \left({f}\left[{v}\right]\ne \varnothing \to \left({f}\left({v}\right)\in {A}\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}\right)\right)\right)\right)\right)$
77 76 imp43 ${⊢}\left(\left({x}\subseteq {A}\wedge {f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\right)\right)\to \left({f}\left[{v}\right]\ne \varnothing \to \left({f}\left({v}\right)\in {A}\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}\right)\right)$
78 39 77 syl5bir ${⊢}\left(\left({x}\subseteq {A}\wedge {f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\right)\right)\to \left(¬{f}\left[{v}\right]=\varnothing \to \left({f}\left({v}\right)\in {A}\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}\right)\right)$
79 inteq ${⊢}{f}\left[{v}\right]=\varnothing \to \bigcap {f}\left[{v}\right]=\bigcap \varnothing$
80 int0 ${⊢}\bigcap \varnothing =\mathrm{V}$
81 79 80 syl6eq ${⊢}{f}\left[{v}\right]=\varnothing \to \bigcap {f}\left[{v}\right]=\mathrm{V}$
82 81 ineq1d ${⊢}{f}\left[{v}\right]=\varnothing \to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)=\mathrm{V}\cap {f}\left({v}\right)$
83 ssv ${⊢}{f}\left({v}\right)\subseteq \mathrm{V}$
84 sseqin2 ${⊢}{f}\left({v}\right)\subseteq \mathrm{V}↔\mathrm{V}\cap {f}\left({v}\right)={f}\left({v}\right)$
85 83 84 mpbi ${⊢}\mathrm{V}\cap {f}\left({v}\right)={f}\left({v}\right)$
86 82 85 syl6eq ${⊢}{f}\left[{v}\right]=\varnothing \to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)={f}\left({v}\right)$
87 86 eleq1d ${⊢}{f}\left[{v}\right]=\varnothing \to \left(\bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}↔{f}\left({v}\right)\in {A}\right)$
88 87 biimprd ${⊢}{f}\left[{v}\right]=\varnothing \to \left({f}\left({v}\right)\in {A}\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}\right)$
89 78 88 pm2.61d2 ${⊢}\left(\left({x}\subseteq {A}\wedge {f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\right)\right)\to \left({f}\left({v}\right)\in {A}\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}\right)$
90 38 89 mpd ${⊢}\left(\left({x}\subseteq {A}\wedge {f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\right)\right)\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}$
91 fvex ${⊢}{f}\left({v}\right)\in \mathrm{V}$
92 91 intunsn ${⊢}\bigcap \left({f}\left[{v}\right]\cup \left\{{f}\left({v}\right)\right\}\right)=\bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)$
93 f1ofn ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {f}Fn\mathrm{suc}{v}$
94 fnsnfv ${⊢}\left({f}Fn\mathrm{suc}{v}\wedge {v}\in \mathrm{suc}{v}\right)\to \left\{{f}\left({v}\right)\right\}={f}\left[\left\{{v}\right\}\right]$
95 93 34 94 sylancl ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \left\{{f}\left({v}\right)\right\}={f}\left[\left\{{v}\right\}\right]$
96 95 uneq2d ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {f}\left[{v}\right]\cup \left\{{f}\left({v}\right)\right\}={f}\left[{v}\right]\cup {f}\left[\left\{{v}\right\}\right]$
97 df-suc ${⊢}\mathrm{suc}{v}={v}\cup \left\{{v}\right\}$
98 97 imaeq2i ${⊢}{f}\left[\mathrm{suc}{v}\right]={f}\left[{v}\cup \left\{{v}\right\}\right]$
99 imaundi ${⊢}{f}\left[{v}\cup \left\{{v}\right\}\right]={f}\left[{v}\right]\cup {f}\left[\left\{{v}\right\}\right]$
100 98 99 eqtr2i ${⊢}{f}\left[{v}\right]\cup {f}\left[\left\{{v}\right\}\right]={f}\left[\mathrm{suc}{v}\right]$
101 96 100 syl6eq ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {f}\left[{v}\right]\cup \left\{{f}\left({v}\right)\right\}={f}\left[\mathrm{suc}{v}\right]$
102 f1ofo ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {f}:\mathrm{suc}{v}\underset{onto}{⟶}{x}$
103 foima ${⊢}{f}:\mathrm{suc}{v}\underset{onto}{⟶}{x}\to {f}\left[\mathrm{suc}{v}\right]={x}$
104 102 103 syl ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {f}\left[\mathrm{suc}{v}\right]={x}$
105 101 104 eqtrd ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to {f}\left[{v}\right]\cup \left\{{f}\left({v}\right)\right\}={x}$
106 105 inteqd ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \bigcap \left({f}\left[{v}\right]\cup \left\{{f}\left({v}\right)\right\}\right)=\bigcap {x}$
107 92 106 syl5eqr ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)=\bigcap {x}$
108 107 eleq1d ${⊢}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \left(\bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}↔\bigcap {x}\in {A}\right)$
109 108 ad2antlr ${⊢}\left(\left({x}\subseteq {A}\wedge {f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\right)\right)\to \left(\bigcap {f}\left[{v}\right]\cap {f}\left({v}\right)\in {A}↔\bigcap {x}\in {A}\right)$
110 90 109 mpbid ${⊢}\left(\left({x}\subseteq {A}\wedge {f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\right)\right)\to \bigcap {x}\in {A}$
111 110 exp43 ${⊢}{x}\subseteq {A}\to \left({f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {x}\in {A}\right)\right)\right)$
112 111 exlimdv ${⊢}{x}\subseteq {A}\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:\mathrm{suc}{v}\underset{1-1 onto}{⟶}{x}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {x}\in {A}\right)\right)\right)$
113 30 112 syl5bi ${⊢}{x}\subseteq {A}\to \left(\mathrm{suc}{v}\approx {x}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {x}\in {A}\right)\right)\right)$
114 113 imp ${⊢}\left({x}\subseteq {A}\wedge \mathrm{suc}{v}\approx {x}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {x}\in {A}\right)\right)$
115 114 adantlr ${⊢}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \mathrm{suc}{v}\approx {x}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {x}\in {A}\right)\right)$
116 115 com13 ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \mathrm{suc}{v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)$
117 28 29 116 alrimd ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \mathrm{suc}{v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)$
118 117 a1i ${⊢}{v}\in \mathrm{\omega }\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge \mathrm{suc}{v}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)\right)$
119 6 10 14 27 118 finds2 ${⊢}{y}\in \mathrm{\omega }\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)$
120 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)\to \bigcap {x}\in {A}\right)\to \left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)\to \bigcap {x}\in {A}\right)$
121 119 120 syl6 ${⊢}{y}\in \mathrm{\omega }\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {y}\approx {x}\right)\to \bigcap {x}\in {A}\right)\right)$
122 121 exp4a ${⊢}{y}\in \mathrm{\omega }\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \left({y}\approx {x}\to \bigcap {x}\in {A}\right)\right)\right)$
123 122 com24 ${⊢}{y}\in \mathrm{\omega }\to \left({y}\approx {x}\to \left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {x}\in {A}\right)\right)\right)$
124 2 123 syl5 ${⊢}{y}\in \mathrm{\omega }\to \left({x}\approx {y}\to \left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {x}\in {A}\right)\right)\right)$
125 124 rexlimiv ${⊢}\exists {y}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}\approx {y}\to \left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {x}\in {A}\right)\right)$
126 1 125 sylbi ${⊢}{x}\in \mathrm{Fin}\to \left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \bigcap {x}\in {A}\right)\right)$
127 126 com13 ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \left({x}\in \mathrm{Fin}\to \bigcap {x}\in {A}\right)\right)$
128 127 impd ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)$
129 128 alrimiv ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)$
130 zfpair2 ${⊢}\left\{{z},{w}\right\}\in \mathrm{V}$
131 sseq1 ${⊢}{x}=\left\{{z},{w}\right\}\to \left({x}\subseteq {A}↔\left\{{z},{w}\right\}\subseteq {A}\right)$
132 neeq1 ${⊢}{x}=\left\{{z},{w}\right\}\to \left({x}\ne \varnothing ↔\left\{{z},{w}\right\}\ne \varnothing \right)$
133 131 132 anbi12d ${⊢}{x}=\left\{{z},{w}\right\}\to \left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)↔\left(\left\{{z},{w}\right\}\subseteq {A}\wedge \left\{{z},{w}\right\}\ne \varnothing \right)\right)$
134 eleq1 ${⊢}{x}=\left\{{z},{w}\right\}\to \left({x}\in \mathrm{Fin}↔\left\{{z},{w}\right\}\in \mathrm{Fin}\right)$
135 133 134 anbi12d ${⊢}{x}=\left\{{z},{w}\right\}\to \left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {x}\in \mathrm{Fin}\right)↔\left(\left(\left\{{z},{w}\right\}\subseteq {A}\wedge \left\{{z},{w}\right\}\ne \varnothing \right)\wedge \left\{{z},{w}\right\}\in \mathrm{Fin}\right)\right)$
136 inteq ${⊢}{x}=\left\{{z},{w}\right\}\to \bigcap {x}=\bigcap \left\{{z},{w}\right\}$
137 136 eleq1d ${⊢}{x}=\left\{{z},{w}\right\}\to \left(\bigcap {x}\in {A}↔\bigcap \left\{{z},{w}\right\}\in {A}\right)$
138 135 137 imbi12d ${⊢}{x}=\left\{{z},{w}\right\}\to \left(\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)↔\left(\left(\left(\left\{{z},{w}\right\}\subseteq {A}\wedge \left\{{z},{w}\right\}\ne \varnothing \right)\wedge \left\{{z},{w}\right\}\in \mathrm{Fin}\right)\to \bigcap \left\{{z},{w}\right\}\in {A}\right)\right)$
139 130 138 spcv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)\to \left(\left(\left(\left\{{z},{w}\right\}\subseteq {A}\wedge \left\{{z},{w}\right\}\ne \varnothing \right)\wedge \left\{{z},{w}\right\}\in \mathrm{Fin}\right)\to \bigcap \left\{{z},{w}\right\}\in {A}\right)$
140 vex ${⊢}{z}\in \mathrm{V}$
141 vex ${⊢}{w}\in \mathrm{V}$
142 140 141 prss ${⊢}\left({z}\in {A}\wedge {w}\in {A}\right)↔\left\{{z},{w}\right\}\subseteq {A}$
143 140 prnz ${⊢}\left\{{z},{w}\right\}\ne \varnothing$
144 143 biantru ${⊢}\left\{{z},{w}\right\}\subseteq {A}↔\left(\left\{{z},{w}\right\}\subseteq {A}\wedge \left\{{z},{w}\right\}\ne \varnothing \right)$
145 prfi ${⊢}\left\{{z},{w}\right\}\in \mathrm{Fin}$
146 145 biantru ${⊢}\left(\left\{{z},{w}\right\}\subseteq {A}\wedge \left\{{z},{w}\right\}\ne \varnothing \right)↔\left(\left(\left\{{z},{w}\right\}\subseteq {A}\wedge \left\{{z},{w}\right\}\ne \varnothing \right)\wedge \left\{{z},{w}\right\}\in \mathrm{Fin}\right)$
147 142 144 146 3bitrri ${⊢}\left(\left(\left\{{z},{w}\right\}\subseteq {A}\wedge \left\{{z},{w}\right\}\ne \varnothing \right)\wedge \left\{{z},{w}\right\}\in \mathrm{Fin}\right)↔\left({z}\in {A}\wedge {w}\in {A}\right)$
148 140 141 intpr ${⊢}\bigcap \left\{{z},{w}\right\}={z}\cap {w}$
149 148 eleq1i ${⊢}\bigcap \left\{{z},{w}\right\}\in {A}↔{z}\cap {w}\in {A}$
150 139 147 149 3imtr3g ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)\to \left(\left({z}\in {A}\wedge {w}\in {A}\right)\to {z}\cap {w}\in {A}\right)$
151 150 ralrimivv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}$
152 129 151 impbii ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)$
153 ineq1 ${⊢}{x}={z}\to {x}\cap {y}={z}\cap {y}$
154 153 eleq1d ${⊢}{x}={z}\to \left({x}\cap {y}\in {A}↔{z}\cap {y}\in {A}\right)$
155 ineq2 ${⊢}{y}={w}\to {z}\cap {y}={z}\cap {w}$
156 155 eleq1d ${⊢}{y}={w}\to \left({z}\cap {y}\in {A}↔{z}\cap {w}\in {A}\right)$
157 154 156 cbvral2vw ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in {A}↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\cap {w}\in {A}$
158 df-3an ${⊢}\left({x}\subseteq {A}\wedge {x}\ne \varnothing \wedge {x}\in \mathrm{Fin}\right)↔\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {x}\in \mathrm{Fin}\right)$
159 158 imbi1i ${⊢}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)↔\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)$
160 159 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)$
161 152 157 160 3bitr4i ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in {A}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \wedge {x}\in \mathrm{Fin}\right)\to \bigcap {x}\in {A}\right)$