iundjiunlem

Description: The sets in the sequence F are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	iundjiunlem.z	$⊢ Z = ℤ_{\geq N}$
	iundjiunlem.f	$⊢ F = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (N ..^n)} E (i))$
	iundjiunlem.j	$⊢ φ \to J \in Z$
	iundjiunlem.k	$⊢ φ \to K \in Z$
	iundjiunlem.lt	$⊢ φ \to J < K$
Assertion	iundjiunlem	$⊢ φ \to F (J) \cap F (K) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		iundjiunlem.z	$⊢ Z = ℤ_{\geq N}$
2		iundjiunlem.f	$⊢ F = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (N ..^n)} E (i))$
3		iundjiunlem.j	$⊢ φ \to J \in Z$
4		iundjiunlem.k	$⊢ φ \to K \in Z$
5		iundjiunlem.lt	$⊢ φ \to J < K$
6		incom	$⊢ F (J) \cap F (K) = F (K) \cap F (J)$
7		simpl	$⊢ (φ \land x \in F (K)) \to φ$
8		simpr	$⊢ (φ \land x \in F (K)) \to x \in F (K)$
9		fveq2	$⊢ n = K \to E (n) = E (K)$
10		oveq2	$⊢ n = K \to (N ..^n) = (N ..^K)$
11	10	iuneq1d	$⊢ n = K \to ⋃_{i \in (N ..^n)} E (i) = ⋃_{i \in (N ..^K)} E (i)$
12	9 11	difeq12d	$⊢ n = K \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) = E (K) ∖ ⋃_{i \in (N ..^K)} E (i)$
13		fvex	$⊢ E (K) \in V$
14	13	difexi	$⊢ E (K) ∖ ⋃_{i \in (N ..^K)} E (i) \in V$
15	12 2 14	fvmpt	$⊢ K \in Z \to F (K) = E (K) ∖ ⋃_{i \in (N ..^K)} E (i)$
16	4 15	syl	$⊢ φ \to F (K) = E (K) ∖ ⋃_{i \in (N ..^K)} E (i)$
17	16	adantr	$⊢ (φ \land x \in F (K)) \to F (K) = E (K) ∖ ⋃_{i \in (N ..^K)} E (i)$
18	8 17	eleqtrd	$⊢ (φ \land x \in F (K)) \to x \in (E (K) ∖ ⋃_{i \in (N ..^K)} E (i))$
19	18	eldifbd	$⊢ (φ \land x \in F (K)) \to \neg x \in ⋃_{i \in (N ..^K)} E (i)$
20	3 1	eleqtrdi	$⊢ φ \to J \in ℤ_{\geq N}$
21	1 4	eluzelz2d	$⊢ φ \to K \in ℤ$
22	20 21 5	elfzod	$⊢ φ \to J \in (N ..^K)$
23		fveq2	$⊢ i = J \to E (i) = E (J)$
24	23	ssiun2s	$⊢ J \in (N ..^K) \to E (J) \subseteq ⋃_{i \in (N ..^K)} E (i)$
25	22 24	syl	$⊢ φ \to E (J) \subseteq ⋃_{i \in (N ..^K)} E (i)$
26	25	ssneld	$⊢ φ \to (\neg x \in ⋃_{i \in (N ..^K)} E (i) \to \neg x \in E (J))$
27	7 19 26	sylc	$⊢ (φ \land x \in F (K)) \to \neg x \in E (J)$
28		eldifi	$⊢ x \in (E (J) ∖ ⋃_{i \in (N ..^J)} E (i)) \to x \in E (J)$
29	27 28	nsyl	$⊢ (φ \land x \in F (K)) \to \neg x \in (E (J) ∖ ⋃_{i \in (N ..^J)} E (i))$
30		fveq2	$⊢ n = J \to E (n) = E (J)$
31		oveq2	$⊢ n = J \to (N ..^n) = (N ..^J)$
32	31	iuneq1d	$⊢ n = J \to ⋃_{i \in (N ..^n)} E (i) = ⋃_{i \in (N ..^J)} E (i)$
33	30 32	difeq12d	$⊢ n = J \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) = E (J) ∖ ⋃_{i \in (N ..^J)} E (i)$
34		fvex	$⊢ E (J) \in V$
35	34	difexi	$⊢ E (J) ∖ ⋃_{i \in (N ..^J)} E (i) \in V$
36	33 2 35	fvmpt	$⊢ J \in Z \to F (J) = E (J) ∖ ⋃_{i \in (N ..^J)} E (i)$
37	3 36	syl	$⊢ φ \to F (J) = E (J) ∖ ⋃_{i \in (N ..^J)} E (i)$
38	37	adantr	$⊢ (φ \land x \in F (K)) \to F (J) = E (J) ∖ ⋃_{i \in (N ..^J)} E (i)$
39	29 38	neleqtrrd	$⊢ (φ \land x \in F (K)) \to \neg x \in F (J)$
40	39	ralrimiva	$⊢ φ \to \forall x \in F (K) \neg x \in F (J)$
41		disj	$⊢ F (K) \cap F (J) = \emptyset \leftrightarrow \forall x \in F (K) \neg x \in F (J)$
42	40 41	sylibr	$⊢ φ \to F (K) \cap F (J) = \emptyset$
43	6 42	syl5eq	$⊢ φ \to F (J) \cap F (K) = \emptyset$

Metamath Proof Explorer

Theorem iundjiunlem

Proof