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