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