iundjiun

Description: Given a sequence E of sets, a sequence F of disjoint sets is built, such that the indexed union stays the same. As in the proof of Property 112C (d) of Fremlin1 p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	iundjiun.nph	$⊢ Ⅎ n φ$
	iundjiun.z	$⊢ Z = ℤ_{\geq N}$
	iundjiun.e	$⊢ φ \to E : Z ⟶ V$
	iundjiun.f	$⊢ F = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (N ..^n)} E (i))$
Assertion	iundjiun	$⊢ φ \to ((\forall m \in Z ⋃_{n = N}^{m} F (n) = ⋃_{n = N}^{m} E (n) \land ⋃_{n \in Z} F (n) = ⋃_{n \in Z} E (n)) \land \underset{n \in Z}{Disj} F (n))$

Proof

Step	Hyp	Ref	Expression
1		iundjiun.nph	$⊢ Ⅎ n φ$
2		iundjiun.z	$⊢ Z = ℤ_{\geq N}$
3		iundjiun.e	$⊢ φ \to E : Z ⟶ V$
4		iundjiun.f	$⊢ F = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (N ..^n)} E (i))$
5		eliun	$⊢ x \in ⋃_{n = N}^{m} F (n) \leftrightarrow \exists n \in (N \dots m) x \in F (n)$
6	5	biimpi	$⊢ x \in ⋃_{n = N}^{m} F (n) \to \exists n \in (N \dots m) x \in F (n)$
7	6	adantl	$⊢ (φ \land x \in ⋃_{n = N}^{m} F (n)) \to \exists n \in (N \dots m) x \in F (n)$
8		nfcv	$⊢ \underline{Ⅎ} n x$
9		nfiu1	$⊢ \underline{Ⅎ} n ⋃_{n = N}^{m} E (n)$
10	8 9	nfel	$⊢ Ⅎ n x \in ⋃_{n = N}^{m} E (n)$
11		simp2	$⊢ (φ \land n \in (N \dots m) \land x \in F (n)) \to n \in (N \dots m)$
12		simpl	$⊢ (φ \land n \in (N \dots m)) \to φ$
13		elfzuz	$⊢ n \in (N \dots m) \to n \in ℤ_{\geq N}$
14	2	eqcomi	$⊢ ℤ_{\geq N} = Z$
15	13 14	eleqtrdi	$⊢ n \in (N \dots m) \to n \in Z$
16	15	adantl	$⊢ (φ \land n \in (N \dots m)) \to n \in Z$
17		simpr	$⊢ (φ \land n \in Z) \to n \in Z$
18	3	ffvelrnda	$⊢ (φ \land n \in Z) \to E (n) \in V$
19		difexg	$⊢ E (n) \in V \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) \in V$
20	18 19	syl	$⊢ (φ \land n \in Z) \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) \in V$
21	4	fvmpt2	$⊢ (n \in Z \land E (n) ∖ ⋃_{i \in (N ..^n)} E (i) \in V) \to F (n) = E (n) ∖ ⋃_{i \in (N ..^n)} E (i)$
22	17 20 21	syl2anc	$⊢ (φ \land n \in Z) \to F (n) = E (n) ∖ ⋃_{i \in (N ..^n)} E (i)$
23		difssd	$⊢ (φ \land n \in Z) \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) \subseteq E (n)$
24	22 23	eqsstrd	$⊢ (φ \land n \in Z) \to F (n) \subseteq E (n)$
25	12 16 24	syl2anc	$⊢ (φ \land n \in (N \dots m)) \to F (n) \subseteq E (n)$
26	25	3adant3	$⊢ (φ \land n \in (N \dots m) \land x \in F (n)) \to F (n) \subseteq E (n)$
27		simp3	$⊢ (φ \land n \in (N \dots m) \land x \in F (n)) \to x \in F (n)$
28	26 27	sseldd	$⊢ (φ \land n \in (N \dots m) \land x \in F (n)) \to x \in E (n)$
29		rspe	$⊢ (n \in (N \dots m) \land x \in E (n)) \to \exists n \in (N \dots m) x \in E (n)$
30	11 28 29	syl2anc	$⊢ (φ \land n \in (N \dots m) \land x \in F (n)) \to \exists n \in (N \dots m) x \in E (n)$
31		eliun	$⊢ x \in ⋃_{n = N}^{m} E (n) \leftrightarrow \exists n \in (N \dots m) x \in E (n)$
32	30 31	sylibr	$⊢ (φ \land n \in (N \dots m) \land x \in F (n)) \to x \in ⋃_{n = N}^{m} E (n)$
33	32	3exp	$⊢ φ \to (n \in (N \dots m) \to (x \in F (n) \to x \in ⋃_{n = N}^{m} E (n)))$
34	1 10 33	rexlimd	$⊢ φ \to (\exists n \in (N \dots m) x \in F (n) \to x \in ⋃_{n = N}^{m} E (n))$
35	34	adantr	$⊢ (φ \land x \in ⋃_{n = N}^{m} F (n)) \to (\exists n \in (N \dots m) x \in F (n) \to x \in ⋃_{n = N}^{m} E (n))$
36	7 35	mpd	$⊢ (φ \land x \in ⋃_{n = N}^{m} F (n)) \to x \in ⋃_{n = N}^{m} E (n)$
37	36	ralrimiva	$⊢ φ \to \forall x \in ⋃_{n = N}^{m} F (n) x \in ⋃_{n = N}^{m} E (n)$
38		dfss3	$⊢ ⋃_{n = N}^{m} F (n) \subseteq ⋃_{n = N}^{m} E (n) \leftrightarrow \forall x \in ⋃_{n = N}^{m} F (n) x \in ⋃_{n = N}^{m} E (n)$
39	37 38	sylibr	$⊢ φ \to ⋃_{n = N}^{m} F (n) \subseteq ⋃_{n = N}^{m} E (n)$
40		fzssuz	$⊢ (N \dots m) \subseteq ℤ_{\geq N}$
41	40	a1i	$⊢ x \in ⋃_{n = N}^{m} E (n) \to (N \dots m) \subseteq ℤ_{\geq N}$
42	31	biimpi	$⊢ x \in ⋃_{n = N}^{m} E (n) \to \exists n \in (N \dots m) x \in E (n)$
43		nfv	$⊢ Ⅎ n x \in E (i)$
44		fveq2	$⊢ n = i \to E (n) = E (i)$
45	44	eleq2d	$⊢ n = i \to (x \in E (n) \leftrightarrow x \in E (i))$
46	43 45	uzwo4	$⊢ ((N \dots m) \subseteq ℤ_{\geq N} \land \exists n \in (N \dots m) x \in E (n)) \to \exists n \in (N \dots m) (x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i)))$
47	41 42 46	syl2anc	$⊢ x \in ⋃_{n = N}^{m} E (n) \to \exists n \in (N \dots m) (x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i)))$
48	47	adantl	$⊢ (φ \land x \in ⋃_{n = N}^{m} E (n)) \to \exists n \in (N \dots m) (x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i)))$
49		simprl	$⊢ ((φ \land n \in (N \dots m)) \land (x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i)))) \to x \in E (n)$
50		nfv	$⊢ Ⅎ i (φ \land n \in (N \dots m))$
51		nfra1	$⊢ Ⅎ i \forall i \in (N \dots m) (i < n \to \neg x \in E (i))$
52	50 51	nfan	$⊢ Ⅎ i ((φ \land n \in (N \dots m)) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i)))$
53		elfzoelz	$⊢ i \in (N ..^n) \to i \in ℤ$
54	53	zred	$⊢ i \in (N ..^n) \to i \in ℝ$
55	54	adantl	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to i \in ℝ$
56		elfzelz	$⊢ n \in (N \dots m) \to n \in ℤ$
57	56	zred	$⊢ n \in (N \dots m) \to n \in ℝ$
58	57	adantr	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to n \in ℝ$
59		1red	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to 1 \in ℝ$
60	58 59	resubcld	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to n - 1 \in ℝ$
61		elfzolem1	$⊢ i \in (N ..^n) \to i \leq n - 1$
62	61	adantl	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to i \leq n - 1$
63	58	ltm1d	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to n - 1 < n$
64	55 60 58 62 63	lelttrd	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to i < n$
65	64	ad4ant24	$⊢ (((φ \land n \in (N \dots m)) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \land i \in (N ..^n)) \to i < n$
66		simplr	$⊢ ((n \in (N \dots m) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \land i \in (N ..^n)) \to \forall i \in (N \dots m) (i < n \to \neg x \in E (i))$
67		elfzel1	$⊢ n \in (N \dots m) \to N \in ℤ$
68	67	adantr	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to N \in ℤ$
69		elfzel2	$⊢ n \in (N \dots m) \to m \in ℤ$
70	69	adantr	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to m \in ℤ$
71	53	adantl	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to i \in ℤ$
72	68 70 71	3jca	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to (N \in ℤ \land m \in ℤ \land i \in ℤ)$
73		elfzole1	$⊢ i \in (N ..^n) \to N \leq i$
74	73	adantl	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to N \leq i$
75	70	zred	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to m \in ℝ$
76		1red	$⊢ n \in (N \dots m) \to 1 \in ℝ$
77	57 76	resubcld	$⊢ n \in (N \dots m) \to n - 1 \in ℝ$
78	69	zred	$⊢ n \in (N \dots m) \to m \in ℝ$
79	57	ltm1d	$⊢ n \in (N \dots m) \to n - 1 < n$
80		elfzle2	$⊢ n \in (N \dots m) \to n \leq m$
81	77 57 78 79 80	ltletrd	$⊢ n \in (N \dots m) \to n - 1 < m$
82	81	adantr	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to n - 1 < m$
83	55 60 75 62 82	lelttrd	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to i < m$
84	55 75 83	ltled	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to i \leq m$
85	72 74 84	jca32	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to ((N \in ℤ \land m \in ℤ \land i \in ℤ) \land (N \leq i \land i \leq m))$
86		elfz2	$⊢ i \in (N \dots m) \leftrightarrow ((N \in ℤ \land m \in ℤ \land i \in ℤ) \land (N \leq i \land i \leq m))$
87	85 86	sylibr	$⊢ (n \in (N \dots m) \land i \in (N ..^n)) \to i \in (N \dots m)$
88	87	adantlr	$⊢ ((n \in (N \dots m) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \land i \in (N ..^n)) \to i \in (N \dots m)$
89		rspa	$⊢ (\forall i \in (N \dots m) (i < n \to \neg x \in E (i)) \land i \in (N \dots m)) \to (i < n \to \neg x \in E (i))$
90	66 88 89	syl2anc	$⊢ ((n \in (N \dots m) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \land i \in (N ..^n)) \to (i < n \to \neg x \in E (i))$
91	90	adantlll	$⊢ (((φ \land n \in (N \dots m)) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \land i \in (N ..^n)) \to (i < n \to \neg x \in E (i))$
92	65 91	mpd	$⊢ (((φ \land n \in (N \dots m)) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \land i \in (N ..^n)) \to \neg x \in E (i)$
93	92	ex	$⊢ ((φ \land n \in (N \dots m)) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \to (i \in (N ..^n) \to \neg x \in E (i))$
94	52 93	ralrimi	$⊢ ((φ \land n \in (N \dots m)) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \to \forall i \in (N ..^n) \neg x \in E (i)$
95		ralnex	$⊢ \forall i \in (N ..^n) \neg x \in E (i) \leftrightarrow \neg \exists i \in (N ..^n) x \in E (i)$
96	94 95	sylib	$⊢ ((φ \land n \in (N \dots m)) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \to \neg \exists i \in (N ..^n) x \in E (i)$
97		eliun	$⊢ x \in ⋃_{i \in (N ..^n)} E (i) \leftrightarrow \exists i \in (N ..^n) x \in E (i)$
98	96 97	sylnibr	$⊢ ((φ \land n \in (N \dots m)) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \to \neg x \in ⋃_{i \in (N ..^n)} E (i)$
99	98	adantrl	$⊢ ((φ \land n \in (N \dots m)) \land (x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i)))) \to \neg x \in ⋃_{i \in (N ..^n)} E (i)$
100	49 99	eldifd	$⊢ ((φ \land n \in (N \dots m)) \land (x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i)))) \to x \in (E (n) ∖ ⋃_{i \in (N ..^n)} E (i))$
101	16 22	syldan	$⊢ (φ \land n \in (N \dots m)) \to F (n) = E (n) ∖ ⋃_{i \in (N ..^n)} E (i)$
102	101	eqcomd	$⊢ (φ \land n \in (N \dots m)) \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) = F (n)$
103	102	adantr	$⊢ ((φ \land n \in (N \dots m)) \land (x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i)))) \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) = F (n)$
104	100 103	eleqtrd	$⊢ ((φ \land n \in (N \dots m)) \land (x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i)))) \to x \in F (n)$
105	104	ex	$⊢ (φ \land n \in (N \dots m)) \to ((x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \to x \in F (n))$
106	105	ex	$⊢ φ \to (n \in (N \dots m) \to ((x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \to x \in F (n)))$
107	1 106	reximdai	$⊢ φ \to (\exists n \in (N \dots m) (x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \to \exists n \in (N \dots m) x \in F (n))$
108	107	adantr	$⊢ (φ \land x \in ⋃_{n = N}^{m} E (n)) \to (\exists n \in (N \dots m) (x \in E (n) \land \forall i \in (N \dots m) (i < n \to \neg x \in E (i))) \to \exists n \in (N \dots m) x \in F (n))$
109	48 108	mpd	$⊢ (φ \land x \in ⋃_{n = N}^{m} E (n)) \to \exists n \in (N \dots m) x \in F (n)$
110	109 5	sylibr	$⊢ (φ \land x \in ⋃_{n = N}^{m} E (n)) \to x \in ⋃_{n = N}^{m} F (n)$
111	39 110	eqelssd	$⊢ φ \to ⋃_{n = N}^{m} F (n) = ⋃_{n = N}^{m} E (n)$
112	111	ralrimivw	$⊢ φ \to \forall m \in Z ⋃_{n = N}^{m} F (n) = ⋃_{n = N}^{m} E (n)$
113	2	iuneqfzuz	$⊢ \forall m \in Z ⋃_{n = N}^{m} F (n) = ⋃_{n = N}^{m} E (n) \to ⋃_{n \in Z} F (n) = ⋃_{n \in Z} E (n)$
114	112 113	syl	$⊢ φ \to ⋃_{n \in Z} F (n) = ⋃_{n \in Z} E (n)$
115		fveq2	$⊢ n = m \to E (n) = E (m)$
116		oveq2	$⊢ n = m \to (N ..^n) = (N ..^m)$
117	116	iuneq1d	$⊢ n = m \to ⋃_{i \in (N ..^n)} E (i) = ⋃_{i \in (N ..^m)} E (i)$
118	115 117	difeq12d	$⊢ n = m \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) = E (m) ∖ ⋃_{i \in (N ..^m)} E (i)$
119	118	cbvmptv	$⊢ (n \in Z ⟼ E (n) ∖ ⋃_{i \in (N ..^n)} E (i)) = (m \in Z ⟼ E (m) ∖ ⋃_{i \in (N ..^m)} E (i))$
120	4 119	eqtri	$⊢ F = (m \in Z ⟼ E (m) ∖ ⋃_{i \in (N ..^m)} E (i))$
121		simpllr	$⊢ (((φ \land n \in Z) \land k \in Z) \land n < k) \to n \in Z$
122		simplr	$⊢ (((φ \land n \in Z) \land k \in Z) \land n < k) \to k \in Z$
123		simpr	$⊢ (((φ \land n \in Z) \land k \in Z) \land n < k) \to n < k$
124	2 120 121 122 123	iundjiunlem	$⊢ (((φ \land n \in Z) \land k \in Z) \land n < k) \to F (n) \cap F (k) = \emptyset$
125	124	adantlr	$⊢ ((((φ \land n \in Z) \land k \in Z) \land \neg n = k) \land n < k) \to F (n) \cap F (k) = \emptyset$
126		simpll	$⊢ ((((φ \land n \in Z) \land k \in Z) \land \neg n = k) \land \neg n < k) \to ((φ \land n \in Z) \land k \in Z)$
127		neqne	$⊢ \neg n = k \to n \neq k$
128		id	$⊢ k \in Z \to k \in Z$
129	128 2	eleqtrdi	$⊢ k \in Z \to k \in ℤ_{\geq N}$
130		eluzelz	$⊢ k \in ℤ_{\geq N} \to k \in ℤ$
131	129 130	syl	$⊢ k \in Z \to k \in ℤ$
132	131	zred	$⊢ k \in Z \to k \in ℝ$
133	132	adantl	$⊢ (n \in Z \land k \in Z) \to k \in ℝ$
134	133	ad2antrr	$⊢ (((n \in Z \land k \in Z) \land n \neq k) \land \neg n < k) \to k \in ℝ$
135		id	$⊢ n \in Z \to n \in Z$
136	135 2	eleqtrdi	$⊢ n \in Z \to n \in ℤ_{\geq N}$
137		eluzelz	$⊢ n \in ℤ_{\geq N} \to n \in ℤ$
138	136 137	syl	$⊢ n \in Z \to n \in ℤ$
139	138	zred	$⊢ n \in Z \to n \in ℝ$
140	139	ad3antrrr	$⊢ (((n \in Z \land k \in Z) \land n \neq k) \land \neg n < k) \to n \in ℝ$
141		simpr	$⊢ ((n \in Z \land k \in Z) \land \neg n < k) \to \neg n < k$
142	133	adantr	$⊢ ((n \in Z \land k \in Z) \land \neg n < k) \to k \in ℝ$
143	139	ad2antrr	$⊢ ((n \in Z \land k \in Z) \land \neg n < k) \to n \in ℝ$
144	142 143	lenltd	$⊢ ((n \in Z \land k \in Z) \land \neg n < k) \to (k \leq n \leftrightarrow \neg n < k)$
145	141 144	mpbird	$⊢ ((n \in Z \land k \in Z) \land \neg n < k) \to k \leq n$
146	145	adantlr	$⊢ (((n \in Z \land k \in Z) \land n \neq k) \land \neg n < k) \to k \leq n$
147		simplr	$⊢ (((n \in Z \land k \in Z) \land n \neq k) \land \neg n < k) \to n \neq k$
148	134 140 146 147	leneltd	$⊢ (((n \in Z \land k \in Z) \land n \neq k) \land \neg n < k) \to k < n$
149	127 148	sylanl2	$⊢ (((n \in Z \land k \in Z) \land \neg n = k) \land \neg n < k) \to k < n$
150	149	ad5ant2345	$⊢ ((((φ \land n \in Z) \land k \in Z) \land \neg n = k) \land \neg n < k) \to k < n$
151		anass	$⊢ ((φ \land n \in Z) \land k \in Z) \leftrightarrow (φ \land (n \in Z \land k \in Z))$
152		incom	$⊢ F (n) \cap F (k) = F (k) \cap F (n)$
153	152	a1i	$⊢ ((φ \land (n \in Z \land k \in Z)) \land k < n) \to F (n) \cap F (k) = F (k) \cap F (n)$
154		simplrr	$⊢ ((φ \land (n \in Z \land k \in Z)) \land k < n) \to k \in Z$
155		simplrl	$⊢ ((φ \land (n \in Z \land k \in Z)) \land k < n) \to n \in Z$
156		simpr	$⊢ ((φ \land (n \in Z \land k \in Z)) \land k < n) \to k < n$
157	2 120 154 155 156	iundjiunlem	$⊢ ((φ \land (n \in Z \land k \in Z)) \land k < n) \to F (k) \cap F (n) = \emptyset$
158	153 157	eqtrd	$⊢ ((φ \land (n \in Z \land k \in Z)) \land k < n) \to F (n) \cap F (k) = \emptyset$
159	151 158	sylanb	$⊢ (((φ \land n \in Z) \land k \in Z) \land k < n) \to F (n) \cap F (k) = \emptyset$
160	126 150 159	syl2anc	$⊢ ((((φ \land n \in Z) \land k \in Z) \land \neg n = k) \land \neg n < k) \to F (n) \cap F (k) = \emptyset$
161	125 160	pm2.61dan	$⊢ (((φ \land n \in Z) \land k \in Z) \land \neg n = k) \to F (n) \cap F (k) = \emptyset$
162	161	ex	$⊢ ((φ \land n \in Z) \land k \in Z) \to (\neg n = k \to F (n) \cap F (k) = \emptyset)$
163		df-or	$⊢ (n = k \lor F (n) \cap F (k) = \emptyset) \leftrightarrow (\neg n = k \to F (n) \cap F (k) = \emptyset)$
164	162 163	sylibr	$⊢ ((φ \land n \in Z) \land k \in Z) \to (n = k \lor F (n) \cap F (k) = \emptyset)$
165	164	ralrimiva	$⊢ (φ \land n \in Z) \to \forall k \in Z (n = k \lor F (n) \cap F (k) = \emptyset)$
166	165	ex	$⊢ φ \to (n \in Z \to \forall k \in Z (n = k \lor F (n) \cap F (k) = \emptyset))$
167	1 166	ralrimi	$⊢ φ \to \forall n \in Z \forall k \in Z (n = k \lor F (n) \cap F (k) = \emptyset)$
168		nfcv	$⊢ \underline{Ⅎ} m F (n)$
169		nfmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ E (n) ∖ ⋃_{i \in (N ..^n)} E (i))$
170	4 169	nfcxfr	$⊢ \underline{Ⅎ} n F$
171		nfcv	$⊢ \underline{Ⅎ} n m$
172	170 171	nffv	$⊢ \underline{Ⅎ} n F (m)$
173		fveq2	$⊢ n = m \to F (n) = F (m)$
174	168 172 173	cbvdisj	$⊢ \underset{n \in Z}{Disj} F (n) \leftrightarrow \underset{m \in Z}{Disj} F (m)$
175		fveq2	$⊢ m = k \to F (m) = F (k)$
176	175	disjor	$⊢ \underset{m \in Z}{Disj} F (m) \leftrightarrow \forall m \in Z \forall k \in Z (m = k \lor F (m) \cap F (k) = \emptyset)$
177		nfcv	$⊢ \underline{Ⅎ} n Z$
178		nfv	$⊢ Ⅎ n m = k$
179		nfcv	$⊢ \underline{Ⅎ} n k$
180	170 179	nffv	$⊢ \underline{Ⅎ} n F (k)$
181	172 180	nfin	$⊢ \underline{Ⅎ} n (F (m) \cap F (k))$
182		nfcv	$⊢ \underline{Ⅎ} n \emptyset$
183	181 182	nfeq	$⊢ Ⅎ n F (m) \cap F (k) = \emptyset$
184	178 183	nfor	$⊢ Ⅎ n (m = k \lor F (m) \cap F (k) = \emptyset)$
185	177 184	nfralw	$⊢ Ⅎ n \forall k \in Z (m = k \lor F (m) \cap F (k) = \emptyset)$
186		nfv	$⊢ Ⅎ m \forall k \in Z (n = k \lor F (n) \cap F (k) = \emptyset)$
187		equequ1	$⊢ m = n \to (m = k \leftrightarrow n = k)$
188		fveq2	$⊢ m = n \to F (m) = F (n)$
189	188	ineq1d	$⊢ m = n \to F (m) \cap F (k) = F (n) \cap F (k)$
190	189	eqeq1d	$⊢ m = n \to (F (m) \cap F (k) = \emptyset \leftrightarrow F (n) \cap F (k) = \emptyset)$
191	187 190	orbi12d	$⊢ m = n \to ((m = k \lor F (m) \cap F (k) = \emptyset) \leftrightarrow (n = k \lor F (n) \cap F (k) = \emptyset))$
192	191	ralbidv	$⊢ m = n \to (\forall k \in Z (m = k \lor F (m) \cap F (k) = \emptyset) \leftrightarrow \forall k \in Z (n = k \lor F (n) \cap F (k) = \emptyset))$
193	185 186 192	cbvralw	$⊢ \forall m \in Z \forall k \in Z (m = k \lor F (m) \cap F (k) = \emptyset) \leftrightarrow \forall n \in Z \forall k \in Z (n = k \lor F (n) \cap F (k) = \emptyset)$
194	174 176 193	3bitri	$⊢ \underset{n \in Z}{Disj} F (n) \leftrightarrow \forall n \in Z \forall k \in Z (n = k \lor F (n) \cap F (k) = \emptyset)$
195	167 194	sylibr	$⊢ φ \to \underset{n \in Z}{Disj} F (n)$
196	112 114 195	jca31	$⊢ φ \to ((\forall m \in Z ⋃_{n = N}^{m} F (n) = ⋃_{n = N}^{m} E (n) \land ⋃_{n \in Z} F (n) = ⋃_{n \in Z} E (n)) \land \underset{n \in Z}{Disj} F (n))$

Metamath Proof Explorer

Theorem iundjiun

Proof