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 28 30 30 3jca ⊢ ( 𝑚 ∈ 𝑍 → ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑚 ∈ ℤ ) )
32 eluzle ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑚 )
33 26 32 syl ⊢ ( 𝑚 ∈ 𝑍 → 𝑁 ≤ 𝑚 )
34 30 zred ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ ℝ )
35 leid ⊢ ( 𝑚 ∈ ℝ → 𝑚 ≤ 𝑚 )
36 34 35 syl ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ≤ 𝑚 )
37 31 33 36 jca32 ⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝑚 ∧ 𝑚 ≤ 𝑚 ) ) )
38 elfz2 ⊢ ( 𝑚 ∈ ( 𝑁 ... 𝑚 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝑚 ∧ 𝑚 ≤ 𝑚 ) ) )
39 37 38 sylibr ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ ( 𝑁 ... 𝑚 ) )
40 nfcv ⊢ Ⅎ 𝑛 𝑥
41 40 3 nfel ⊢ Ⅎ 𝑛 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴
42 4 eleq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
43 41 42 rspce ⊢ ( ( 𝑚 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ 𝐴 )
44 39 43 sylan ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ 𝐴 )
45 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 ↔ ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ 𝐴 )
46 44 45 sylibr ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 )
47 46 3adant2 ⊢ ( ( 𝑚 ∈ 𝑍 ∧ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 )
48 24 47 sseldd ⊢ ( ( 𝑚 ∈ 𝑍 ∧ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 )
49 13 15 16 48 syl3anc ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 )
50 49 3exp ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ( 𝑚 ∈ 𝑍 → ( 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 ) ) )
51 11 12 50 rexlimd ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ( ∃ 𝑚 ∈ 𝑍 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 ) )
52 51 adantr ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 ) → ( ∃ 𝑚 ∈ 𝑍 𝑥 ∈ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 ) )
53 10 52 mpd ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 )
54 53 ralrimiva ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∀ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 )
55 dfss3 ⊢ ( ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵 ↔ ∀ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵 )
56 54 55 sylibr ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵 )