Metamath Proof Explorer

Theorem iuneqfzuzlem

Description: Lemma for iuneqfzuz : here, inclusion is proven; aiuneqfzuz uses this lemma twice, to prove equality. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis iuneqfzuzlem.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
Assertion iuneqfzuzlem ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵 )

Proof

Step Hyp Ref Expression
1 iuneqfzuzlem.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
2 nfcv ⊢ Ⅎ 𝑚 𝐴
3 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴
4 csbeq1a ⊢ ( 𝑛 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
5 2 3 4 cbviun ⊢ ∪ 𝑛 ∈ 𝑍 𝐴 = ∪ 𝑚 ∈ 𝑍 ⦋ 𝑚 / 𝑛 ⦌ 𝐴
6 5 eleq2i ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 ↔ 𝑥 ∈ ∪ 𝑚 ∈ 𝑍 ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
7 eliun ⊢ ( 𝑥 ∈ ∪ 𝑚 ∈ 𝑍 ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ↔ ∃ 𝑚 ∈ 𝑍 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
8 6 7 bitri ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 ↔ ∃ 𝑚 ∈ 𝑍 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
9 8 biimpi ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 → ∃ 𝑚 ∈ 𝑍 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
10 9 adantl ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 ) → ∃ 𝑚 ∈ 𝑍 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
11 nfra1 ⊢ Ⅎ 𝑚 ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵
12 nfv ⊢ Ⅎ 𝑚 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵
13 simp2 ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → 𝑚 ∈ 𝑍 )
14 rspa ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑚 ∈ 𝑍 ) → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 )
15 14 3adant3 ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 )
16 simp3 ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
17 id ⊢ ( ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 )
18 fzssuz ⊢ ( 𝑁 ... 𝑚 ) ⊆ ( ℤ≥ ‘ 𝑁 )
19 1 eqcomi ⊢ ( ℤ≥ ‘ 𝑁 ) = 𝑍
20 18 19 sseqtri ⊢ ( 𝑁 ... 𝑚 ) ⊆ 𝑍
21 iunss1 ⊢ ( ( 𝑁 ... 𝑚 ) ⊆ 𝑍 → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵 )
22 20 21 mp1i ⊢ ( ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵 )
23 17 22 eqsstrd ⊢ ( ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵 )
24 23 3ad2ant2 ⊢ ( ( 𝑚 ∈ 𝑍 ∧ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵 )
25 1 eleq2i ⊢ ( 𝑚 ∈ 𝑍 ↔ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) )
26 25 biimpi ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) )
27 eluzel2 ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ∈ ℤ )
28 26 27 syl ⊢ ( 𝑚 ∈ 𝑍 → 𝑁 ∈ ℤ )
29 eluzelz ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑚 ∈ ℤ )
30 26 29 syl ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ ℤ )
31 eluzle ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑚 )
32 26 31 syl ⊢ ( 𝑚 ∈ 𝑍 → 𝑁 ≤ 𝑚 )
33 30 zred ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ ℝ )
34 leid ⊢ ( 𝑚 ∈ ℝ → 𝑚 ≤ 𝑚 )
35 33 34 syl ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ≤ 𝑚 )
36 28 30 30 32 35 elfzd ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ ( 𝑁 ... 𝑚 ) )
37 nfcv ⊢ Ⅎ 𝑛 𝑥
38 37 3 nfel ⊢ Ⅎ 𝑛 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴
39 4 eleq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
40 38 39 rspce ⊢ ( ( 𝑚 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ 𝐴 )
41 36 40 sylan ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ 𝐴 )
42 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 ↔ ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ 𝐴 )
43 41 42 sylibr ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 )
44 43 3adant2 ⊢ ( ( 𝑚 ∈ 𝑍 ∧ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 )
45 24 44 sseldd ⊢ ( ( 𝑚 ∈ 𝑍 ∧ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 )
46 13 15 16 45 syl3anc ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 )
47 46 3exp ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ( 𝑚 ∈ 𝑍 → ( 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 ) ) )
48 11 12 47 rexlimd ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ( ∃ 𝑚 ∈ 𝑍 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 ) )
49 48 adantr ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 ) → ( ∃ 𝑚 ∈ 𝑍 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 ) )
50 10 49 mpd ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 )
51 50 ralrimiva ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∀ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 )
52 dfss3 ⊢ ( ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵 ↔ ∀ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 )
53 51 52 sylibr ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵 )