Theorem iuneqfzuzlem 45791

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

Hypothesis

Ref	Expression
iuneqfzuzlem.z	⊢ 𝑍 = (ℤ≥‘𝑁)

Assertion

Ref	Expression
iuneqfzuzlem	⊢ (∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵)

Distinct variable groups:   𝐴,𝑚   𝐵,𝑚   𝑛,𝑁   𝑚,𝑍,𝑛

Allowed substitution hints:   𝐴(𝑛)   𝐵(𝑛)   𝑁(𝑚)

Proof of Theorem iuneqfzuzlem

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfcv 2903	. . . . . . . 8 ⊢ Ⅎ𝑚𝐴
2		nfcsb1v 3856	. . . . . . . 8 ⊢ Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴
3		csbeq1a 3846	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴)
4	1, 2, 3	cbviun 4966	. . . . . . 7 ⊢ ∪ 𝑛 ∈ 𝑍 𝐴 = ∪ 𝑚 ∈ 𝑍 ⦋𝑚 / 𝑛⦌𝐴
5	4	eleq2i 2833	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 ↔ 𝑥 ∈ ∪ 𝑚 ∈ 𝑍 ⦋𝑚 / 𝑛⦌𝐴)
6		eliun 4927	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑚 ∈ 𝑍 ⦋𝑚 / 𝑛⦌𝐴 ↔ ∃𝑚 ∈ 𝑍 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴)
7	5, 6	bitri 277	. . . . 5 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴 ↔ ∃𝑚 ∈ 𝑍 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴)
8	7	bilani 506	. . . 4 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴) → ∃𝑚 ∈ 𝑍 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴)
9		nfra1 3265	. . . . . 6 ⊢ Ⅎ𝑚∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵
10		nfv 1922	. . . . . 6 ⊢ Ⅎ𝑚 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵
11		simp2 1144	. . . . . . . 8 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴) → 𝑚 ∈ 𝑍)
12		rspa 3230	. . . . . . . . 9 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵)
13	12	3adant3 1139	. . . . . . . 8 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴) → ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵)
14		simp3 1145	. . . . . . . 8 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴) → 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴)
15		id 22	. . . . . . . . . . 11 ⊢ (∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵)
16		fzssuz 13514	. . . . . . . . . . . . 13 ⊢ (𝑁...𝑚) ⊆ (ℤ≥‘𝑁)
17		iuneqfzuzlem.z	. . . . . . . . . . . . . 14 ⊢ 𝑍 = (ℤ≥‘𝑁)
18	17	eqcomi 2750	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘𝑁) = 𝑍
19	16, 18	sseqtri 3964	. . . . . . . . . . . 12 ⊢ (𝑁...𝑚) ⊆ 𝑍
20		iunss1 4938	. . . . . . . . . . . 12 ⊢ ((𝑁...𝑚) ⊆ 𝑍 → ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵)
21	19, 20	mp1i 13	. . . . . . . . . . 11 ⊢ (∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵)
22	15, 21	eqsstrd 3950	. . . . . . . . . 10 ⊢ (∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵)
23	22	3ad2ant2 1141	. . . . . . . . 9 ⊢ ((𝑚 ∈ 𝑍 ∧ ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ∧ 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴) → ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵)
24	17	eleq2i 2833	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ 𝑍 ↔ 𝑚 ∈ (ℤ≥‘𝑁))
25	24	biimpi 218	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ (ℤ≥‘𝑁))
26		eluzel2 12788	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (ℤ≥‘𝑁) → 𝑁 ∈ ℤ)
27	25, 26	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ 𝑍 → 𝑁 ∈ ℤ)
28		eluzelz 12793	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (ℤ≥‘𝑁) → 𝑚 ∈ ℤ)
29	25, 28	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ ℤ)
30		eluzle 12796	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (ℤ≥‘𝑁) → 𝑁 ≤ 𝑚)
31	25, 30	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ 𝑍 → 𝑁 ≤ 𝑚)
32	29	zred 12628	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ ℝ)
33		leid 11238	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℝ → 𝑚 ≤ 𝑚)
34	32, 33	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ 𝑍 → 𝑚 ≤ 𝑚)
35	27, 29, 29, 31, 34	elfzd 13464	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ (𝑁...𝑚))
36		nfcv 2903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛𝑥
37	36, 2	nfel 2917	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴
38	3	eleq2d 2827	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴))
39	37, 38	rspce 3550	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ 𝐴)
40	35, 39	sylan 587	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ 𝐴)
41		eliun 4927	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ 𝐴)
42	40, 41	sylibr 236	. . . . . . . . . 10 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴) → 𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)𝐴)
43	42	3adant2 1138	. . . . . . . . 9 ⊢ ((𝑚 ∈ 𝑍 ∧ ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ∧ 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴) → 𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)𝐴)
44	23, 43	sseldd 3917	. . . . . . . 8 ⊢ ((𝑚 ∈ 𝑍 ∧ ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ∧ 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵)
45	11, 13, 14, 44	syl3anc 1380	. . . . . . 7 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵)
46	45	3exp 1126	. . . . . 6 ⊢ (∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → (𝑚 ∈ 𝑍 → (𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵)))
47	9, 10, 46	rexlimd 3248	. . . . 5 ⊢ (∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → (∃𝑚 ∈ 𝑍 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵))
48	47	adantr 482	. . . 4 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴) → (∃𝑚 ∈ 𝑍 𝑥 ∈ ⦋𝑚 / 𝑛⦌𝐴 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵))
49	8, 48	mpd 15	. . 3 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵)
50	49	ralrimiva 3133	. 2 ⊢ (∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → ∀𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵)
51		dfss3 3905	. 2 ⊢ (∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵 ↔ ∀𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐴𝑥 ∈ ∪ 𝑛 ∈ 𝑍 𝐵)
52	50, 51	sylibr 236	1 ⊢ (∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093   = wceq 1548   ∈ wcel 2121  ∀wral 3055  ∃wrex 3065  ⦋csb 3832   ⊆ wss 3884  ∪ ciun 4923   class class class wbr 5074  ‘cfv 6488  (class class class)co 7359  ℝcr 11033   ≤ cle 11176  ℤcz 12519  ℤ_≥cuz 12783  ...cfz 13456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7681  ax-cnex 11090  ax-resscn 11091  ax-pre-lttri 11108

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3725  df-csb 3833  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-ov 7362  df-oprab 7363  df-mpo 7364  df-1st 7933  df-2nd 7934  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11177  df-mnf 11178  df-xr 11179  df-ltxr 11180  df-le 11181  df-neg 11376  df-z 12520  df-uz 12784  df-fz 13457

This theorem is referenced by:  iuneqfzuz  45792