Theorem iundjiunlem

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

	Ref	Expression
Hypotheses	iundjiunlem.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
	iundjiunlem.f	⊢ 𝐹 = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
	iundjiunlem.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑍 )
	iundjiunlem.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑍 )
	iundjiunlem.lt	⊢ ( 𝜑 → 𝐽 < 𝐾 )
Assertion	iundjiunlem	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐽 ) ∩ ( 𝐹 ‘ 𝐾 ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		iundjiunlem.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
2		iundjiunlem.f	⊢ 𝐹 = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
3		iundjiunlem.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑍 )
4		iundjiunlem.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑍 )
5		iundjiunlem.lt	⊢ ( 𝜑 → 𝐽 < 𝐾 )
6		incom	⊢ ( ( 𝐹 ‘ 𝐽 ) ∩ ( 𝐹 ‘ 𝐾 ) ) = ( ( 𝐹 ‘ 𝐾 ) ∩ ( 𝐹 ‘ 𝐽 ) )
7		simpl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) ) → 𝜑 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) ) → 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) )
9		fveq2	⊢ ( 𝑛 = 𝐾 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝐾 ) )
10		oveq2	⊢ ( 𝑛 = 𝐾 → ( 𝑁 ..^ 𝑛 ) = ( 𝑁 ..^ 𝐾 ) )
11	10	iuneq1d	⊢ ( 𝑛 = 𝐾 → ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐾 ) ( 𝐸 ‘ 𝑖 ) )
12	9 11	difeq12d	⊢ ( 𝑛 = 𝐾 → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ 𝐾 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐾 ) ( 𝐸 ‘ 𝑖 ) ) )
13		fvex	⊢ ( 𝐸 ‘ 𝐾 ) ∈ V
14	13	difexi	⊢ ( ( 𝐸 ‘ 𝐾 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐾 ) ( 𝐸 ‘ 𝑖 ) ) ∈ V
15	12 2 14	fvmpt	⊢ ( 𝐾 ∈ 𝑍 → ( 𝐹 ‘ 𝐾 ) = ( ( 𝐸 ‘ 𝐾 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐾 ) ( 𝐸 ‘ 𝑖 ) ) )
16	4 15	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) = ( ( 𝐸 ‘ 𝐾 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐾 ) ( 𝐸 ‘ 𝑖 ) ) )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝐾 ) = ( ( 𝐸 ‘ 𝐾 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐾 ) ( 𝐸 ‘ 𝑖 ) ) )
18	8 17	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) ) → 𝑥 ∈ ( ( 𝐸 ‘ 𝐾 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐾 ) ( 𝐸 ‘ 𝑖 ) ) )
19	18	eldifbd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) ) → ¬ 𝑥 ∈ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐾 ) ( 𝐸 ‘ 𝑖 ) )
20	3 1	eleqtrdi	⊢ ( 𝜑 → 𝐽 ∈ ( ℤ≥ ‘ 𝑁 ) )
21	1 4	eluzelz2d	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
22	20 21 5	elfzod	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑁 ..^ 𝐾 ) )
23		fveq2	⊢ ( 𝑖 = 𝐽 → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝐽 ) )
24	23	ssiun2s	⊢ ( 𝐽 ∈ ( 𝑁 ..^ 𝐾 ) → ( 𝐸 ‘ 𝐽 ) ⊆ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐾 ) ( 𝐸 ‘ 𝑖 ) )
25	22 24	syl	⊢ ( 𝜑 → ( 𝐸 ‘ 𝐽 ) ⊆ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐾 ) ( 𝐸 ‘ 𝑖 ) )
26	25	ssneld	⊢ ( 𝜑 → ( ¬ 𝑥 ∈ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐾 ) ( 𝐸 ‘ 𝑖 ) → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝐽 ) ) )
27	7 19 26	sylc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) ) → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝐽 ) )
28		eldifi	⊢ ( 𝑥 ∈ ( ( 𝐸 ‘ 𝐽 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐽 ) ( 𝐸 ‘ 𝑖 ) ) → 𝑥 ∈ ( 𝐸 ‘ 𝐽 ) )
29	27 28	nsyl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) ) → ¬ 𝑥 ∈ ( ( 𝐸 ‘ 𝐽 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐽 ) ( 𝐸 ‘ 𝑖 ) ) )
30		fveq2	⊢ ( 𝑛 = 𝐽 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝐽 ) )
31		oveq2	⊢ ( 𝑛 = 𝐽 → ( 𝑁 ..^ 𝑛 ) = ( 𝑁 ..^ 𝐽 ) )
32	31	iuneq1d	⊢ ( 𝑛 = 𝐽 → ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐽 ) ( 𝐸 ‘ 𝑖 ) )
33	30 32	difeq12d	⊢ ( 𝑛 = 𝐽 → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ 𝐽 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐽 ) ( 𝐸 ‘ 𝑖 ) ) )
34		fvex	⊢ ( 𝐸 ‘ 𝐽 ) ∈ V
35	34	difexi	⊢ ( ( 𝐸 ‘ 𝐽 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐽 ) ( 𝐸 ‘ 𝑖 ) ) ∈ V
36	33 2 35	fvmpt	⊢ ( 𝐽 ∈ 𝑍 → ( 𝐹 ‘ 𝐽 ) = ( ( 𝐸 ‘ 𝐽 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐽 ) ( 𝐸 ‘ 𝑖 ) ) )
37	3 36	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐽 ) = ( ( 𝐸 ‘ 𝐽 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐽 ) ( 𝐸 ‘ 𝑖 ) ) )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝐽 ) = ( ( 𝐸 ‘ 𝐽 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝐽 ) ( 𝐸 ‘ 𝑖 ) ) )
39	29 38	neleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) ) → ¬ 𝑥 ∈ ( 𝐹 ‘ 𝐽 ) )
40	39	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) ¬ 𝑥 ∈ ( 𝐹 ‘ 𝐽 ) )
41		disj	⊢ ( ( ( 𝐹 ‘ 𝐾 ) ∩ ( 𝐹 ‘ 𝐽 ) ) = ∅ ↔ ∀ 𝑥 ∈ ( 𝐹 ‘ 𝐾 ) ¬ 𝑥 ∈ ( 𝐹 ‘ 𝐽 ) )
42	40 41	sylibr	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐾 ) ∩ ( 𝐹 ‘ 𝐽 ) ) = ∅ )
43	6 42	syl5eq	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐽 ) ∩ ( 𝐹 ‘ 𝐾 ) ) = ∅ )