Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  iundjiun Structured version   Visualization version   GIF version

Theorem iundjiun 40995
Description: Given a sequence 𝐸 of sets, a sequence 𝐹 of disjoint sets is built, such that the indexed union stays the same. As in the proof of Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
iundjiun.nph 𝑛𝜑
iundjiun.z 𝑍 = (ℤ𝑁)
iundjiun.e (𝜑𝐸:𝑍𝑉)
iundjiun.f 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
Assertion
Ref Expression
iundjiun (𝜑 → ((∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ∧ 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛)) ∧ Disj 𝑛𝑍 (𝐹𝑛)))
Distinct variable groups:   𝑖,𝐸,𝑚,𝑛   𝑚,𝐹   𝑖,𝑁,𝑚,𝑛   𝑚,𝑍,𝑛   𝜑,𝑖,𝑚
Allowed substitution hints:   𝜑(𝑛)   𝐹(𝑖,𝑛)   𝑉(𝑖,𝑚,𝑛)   𝑍(𝑖)

Proof of Theorem iundjiun
Dummy variables 𝑥 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eliun 4556 . . . . . . . . 9 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
21biimpi 206 . . . . . . . 8 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
32adantl 481 . . . . . . 7 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
4 iundjiun.nph . . . . . . . . 9 𝑛𝜑
5 nfcv 2793 . . . . . . . . . 10 𝑛𝑥
6 nfiu1 4582 . . . . . . . . . 10 𝑛 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)
75, 6nfel 2806 . . . . . . . . 9 𝑛 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)
8 simp2 1082 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑛 ∈ (𝑁...𝑚))
9 simpl 472 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (𝑁...𝑚)) → 𝜑)
10 elfzuz 12376 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ (ℤ𝑁))
11 iundjiun.z . . . . . . . . . . . . . . . . . 18 𝑍 = (ℤ𝑁)
1211eqcomi 2660 . . . . . . . . . . . . . . . . 17 (ℤ𝑁) = 𝑍
1310, 12syl6eleq 2740 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (𝑁...𝑚) → 𝑛𝑍)
1413adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (𝑁...𝑚)) → 𝑛𝑍)
15 simpr 476 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → 𝑛𝑍)
16 iundjiun.e . . . . . . . . . . . . . . . . . . 19 (𝜑𝐸:𝑍𝑉)
1716ffvelrnda 6399 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝑍) → (𝐸𝑛) ∈ 𝑉)
18 difexg 4841 . . . . . . . . . . . . . . . . . 18 ((𝐸𝑛) ∈ 𝑉 → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ V)
1917, 18syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ V)
20 iundjiun.f . . . . . . . . . . . . . . . . . 18 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
2120fvmpt2 6330 . . . . . . . . . . . . . . . . 17 ((𝑛𝑍 ∧ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ V) → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
2215, 19, 21syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
23 difssd 3771 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ⊆ (𝐸𝑛))
2422, 23eqsstrd 3672 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍) → (𝐹𝑛) ⊆ (𝐸𝑛))
259, 14, 24syl2anc 694 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (𝑁...𝑚)) → (𝐹𝑛) ⊆ (𝐸𝑛))
26253adant3 1101 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → (𝐹𝑛) ⊆ (𝐸𝑛))
27 simp3 1083 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑥 ∈ (𝐹𝑛))
2826, 27sseldd 3637 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑥 ∈ (𝐸𝑛))
29 rspe 3032 . . . . . . . . . . . 12 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
308, 28, 29syl2anc 694 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
31 eliun 4556 . . . . . . . . . . 11 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
3230, 31sylibr 224 . . . . . . . . . 10 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
33323exp 1283 . . . . . . . . 9 (𝜑 → (𝑛 ∈ (𝑁...𝑚) → (𝑥 ∈ (𝐹𝑛) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))))
344, 7, 33rexlimd 3055 . . . . . . . 8 (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)))
3534adantr 480 . . . . . . 7 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)))
363, 35mpd 15 . . . . . 6 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
3736ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
38 dfss3 3625 . . . . 5 ( 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) ⊆ 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ↔ ∀𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
3937, 38sylibr 224 . . . 4 (𝜑 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) ⊆ 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
40 fzssuz 12420 . . . . . . . . . . 11 (𝑁...𝑚) ⊆ (ℤ𝑁)
4140a1i 11 . . . . . . . . . 10 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → (𝑁...𝑚) ⊆ (ℤ𝑁))
4231biimpi 206 . . . . . . . . . 10 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
43 nfv 1883 . . . . . . . . . . 11 𝑛 𝑥 ∈ (𝐸𝑖)
44 fveq2 6229 . . . . . . . . . . . 12 (𝑛 = 𝑖 → (𝐸𝑛) = (𝐸𝑖))
4544eleq2d 2716 . . . . . . . . . . 11 (𝑛 = 𝑖 → (𝑥 ∈ (𝐸𝑛) ↔ 𝑥 ∈ (𝐸𝑖)))
4643, 45uzwo4 39535 . . . . . . . . . 10 (((𝑁...𝑚) ⊆ (ℤ𝑁) ∧ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))))
4741, 42, 46syl2anc 694 . . . . . . . . 9 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))))
4847adantl 481 . . . . . . . 8 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))))
49 simprl 809 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → 𝑥 ∈ (𝐸𝑛))
50 nfv 1883 . . . . . . . . . . . . . . . . . . 19 𝑖(𝜑𝑛 ∈ (𝑁...𝑚))
51 nfra1 2970 . . . . . . . . . . . . . . . . . . 19 𝑖𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))
5250, 51nfan 1868 . . . . . . . . . . . . . . . . . 18 𝑖((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
53 elfzoelz 12509 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℤ)
5453zred 11520 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℝ)
5554adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℝ)
56 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℤ)
5756zred 11520 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℝ)
5857adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑛 ∈ ℝ)
59 1red 10093 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 1 ∈ ℝ)
6058, 59resubcld 10496 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) ∈ ℝ)
61 elfzolem1 39850 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ≤ (𝑛 − 1))
6261adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ≤ (𝑛 − 1))
6358ltm1d 10994 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑛)
6455, 60, 58, 62, 63lelttrd 10233 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛)
6564ad4ant24 1327 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛)
66 simplr 807 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
67 elfzel1 12379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (𝑁...𝑚) → 𝑁 ∈ ℤ)
6867adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁 ∈ ℤ)
69 elfzel2 12378 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℤ)
7069adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℤ)
7153adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℤ)
7268, 70, 713jca 1261 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ))
73 elfzole1 12517 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (𝑁..^𝑛) → 𝑁𝑖)
7473adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁𝑖)
7570zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℝ)
76 1red 10093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 ∈ (𝑁...𝑚) → 1 ∈ ℝ)
7757, 76resubcld 10496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) ∈ ℝ)
7869zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℝ)
7957ltm1d 10994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑛)
80 elfzle2 12383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ (𝑁...𝑚) → 𝑛𝑚)
8177, 57, 78, 79, 80ltletrd 10235 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑚)
8281adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑚)
8355, 60, 75, 62, 82lelttrd 10233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑚)
8455, 75, 83ltled 10223 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖𝑚)
8572, 74, 84jca32 557 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑁𝑖𝑖𝑚)))
86 elfz2 12371 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (𝑁...𝑚) ↔ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑁𝑖𝑖𝑚)))
8785, 86sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚))
8887adantlr 751 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚))
89 rspa 2959 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)) ∧ 𝑖 ∈ (𝑁...𝑚)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
9066, 88, 89syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
9190adantlll 754 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
9265, 91mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ¬ 𝑥 ∈ (𝐸𝑖))
9392ex 449 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → (𝑖 ∈ (𝑁..^𝑛) → ¬ 𝑥 ∈ (𝐸𝑖)))
9452, 93ralrimi 2986 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ∀𝑖 ∈ (𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸𝑖))
95 ralnex 3021 . . . . . . . . . . . . . . . . 17 (∀𝑖 ∈ (𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸𝑖) ↔ ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸𝑖))
9694, 95sylib 208 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸𝑖))
97 eliun 4556 . . . . . . . . . . . . . . . 16 (𝑥 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖) ↔ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸𝑖))
9896, 97sylnibr 318 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ¬ 𝑥 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖))
9998adantrl 752 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → ¬ 𝑥 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖))
10049, 99eldifd 3618 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → 𝑥 ∈ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
10114, 22syldan 486 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (𝑁...𝑚)) → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
102101eqcomd 2657 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (𝑁...𝑚)) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) = (𝐹𝑛))
103102adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) = (𝐹𝑛))
104100, 103eleqtrd 2732 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → 𝑥 ∈ (𝐹𝑛))
105104ex 449 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑁...𝑚)) → ((𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → 𝑥 ∈ (𝐹𝑛)))
106105ex 449 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ (𝑁...𝑚) → ((𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → 𝑥 ∈ (𝐹𝑛))))
1074, 106reximdai 3041 . . . . . . . . 9 (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛)))
108107adantr 480 . . . . . . . 8 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛)))
10948, 108mpd 15 . . . . . . 7 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
110109, 1sylibr 224 . . . . . 6 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛))
111110ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛))
112 dfss3 3625 . . . . 5 ( 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ⊆ 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) ↔ ∀𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛))
113111, 112sylibr 224 . . . 4 (𝜑 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ⊆ 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛))
11439, 113eqssd 3653 . . 3 (𝜑 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
115114ralrimivw 2996 . 2 (𝜑 → ∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
11611iuneqfzuz 39864 . . 3 (∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛))
117115, 116syl 17 . 2 (𝜑 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛))
118 fveq2 6229 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → (𝐸𝑛) = (𝐸𝑚))
119 oveq2 6698 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝑁..^𝑛) = (𝑁..^𝑚))
120119iuneq1d 4577 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖))
121118, 120difeq12d 3762 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) = ((𝐸𝑚) ∖ 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖)))
122121cbvmptv 4783 . . . . . . . . . . . 12 (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖))) = (𝑚𝑍 ↦ ((𝐸𝑚) ∖ 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖)))
12320, 122eqtri 2673 . . . . . . . . . . 11 𝐹 = (𝑚𝑍 ↦ ((𝐸𝑚) ∖ 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖)))
124 simpllr 815 . . . . . . . . . . 11 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → 𝑛𝑍)
125 simplr 807 . . . . . . . . . . 11 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → 𝑘𝑍)
126 simpr 476 . . . . . . . . . . 11 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → 𝑛 < 𝑘)
12711, 123, 124, 125, 126iundjiunlem 40994 . . . . . . . . . 10 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
128127adantlr 751 . . . . . . . . 9 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ 𝑛 < 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
129 simpll 805 . . . . . . . . . 10 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝜑𝑛𝑍) ∧ 𝑘𝑍))
130 neqne 2831 . . . . . . . . . . . 12 𝑛 = 𝑘𝑛𝑘)
131 id 22 . . . . . . . . . . . . . . . . . 18 (𝑘𝑍𝑘𝑍)
132131, 11syl6eleq 2740 . . . . . . . . . . . . . . . . 17 (𝑘𝑍𝑘 ∈ (ℤ𝑁))
133 eluzelz 11735 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ𝑁) → 𝑘 ∈ ℤ)
134132, 133syl 17 . . . . . . . . . . . . . . . 16 (𝑘𝑍𝑘 ∈ ℤ)
135134zred 11520 . . . . . . . . . . . . . . 15 (𝑘𝑍𝑘 ∈ ℝ)
136135adantl 481 . . . . . . . . . . . . . 14 ((𝑛𝑍𝑘𝑍) → 𝑘 ∈ ℝ)
137136ad2antrr 762 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ)
138 id 22 . . . . . . . . . . . . . . . . 17 (𝑛𝑍𝑛𝑍)
139138, 11syl6eleq 2740 . . . . . . . . . . . . . . . 16 (𝑛𝑍𝑛 ∈ (ℤ𝑁))
140 eluzelz 11735 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ𝑁) → 𝑛 ∈ ℤ)
141139, 140syl 17 . . . . . . . . . . . . . . 15 (𝑛𝑍𝑛 ∈ ℤ)
142141zred 11520 . . . . . . . . . . . . . 14 (𝑛𝑍𝑛 ∈ ℝ)
143142ad3antrrr 766 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ)
144 simpr 476 . . . . . . . . . . . . . . 15 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → ¬ 𝑛 < 𝑘)
145136adantr 480 . . . . . . . . . . . . . . . 16 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ)
146142ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ)
147145, 146lenltd 10221 . . . . . . . . . . . . . . 15 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → (𝑘𝑛 ↔ ¬ 𝑛 < 𝑘))
148144, 147mpbird 247 . . . . . . . . . . . . . 14 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘𝑛)
149148adantlr 751 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘𝑛)
150 simplr 807 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛𝑘)
151137, 143, 149, 150leneltd 10229 . . . . . . . . . . . 12 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛)
152130, 151sylanl2 684 . . . . . . . . . . 11 ((((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛)
153152ad5ant2345 1357 . . . . . . . . . 10 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛)
154 anass 682 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑘𝑍) ↔ (𝜑 ∧ (𝑛𝑍𝑘𝑍)))
155 incom 3838 . . . . . . . . . . . . 13 ((𝐹𝑛) ∩ (𝐹𝑘)) = ((𝐹𝑘) ∩ (𝐹𝑛))
156155a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ((𝐹𝑘) ∩ (𝐹𝑛)))
157 simplrr 818 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → 𝑘𝑍)
158 simplrl 817 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → 𝑛𝑍)
159 simpr 476 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → 𝑘 < 𝑛)
16011, 123, 157, 158, 159iundjiunlem 40994 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹𝑘) ∩ (𝐹𝑛)) = ∅)
161156, 160eqtrd 2685 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
162154, 161sylanb 488 . . . . . . . . . 10 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑘 < 𝑛) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
163129, 153, 162syl2anc 694 . . . . . . . . 9 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
164128, 163pm2.61dan 849 . . . . . . . 8 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
165164ex 449 . . . . . . 7 (((𝜑𝑛𝑍) ∧ 𝑘𝑍) → (¬ 𝑛 = 𝑘 → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
166 df-or 384 . . . . . . 7 ((𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅) ↔ (¬ 𝑛 = 𝑘 → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
167165, 166sylibr 224 . . . . . 6 (((𝜑𝑛𝑍) ∧ 𝑘𝑍) → (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
168167ralrimiva 2995 . . . . 5 ((𝜑𝑛𝑍) → ∀𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
169168ex 449 . . . 4 (𝜑 → (𝑛𝑍 → ∀𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)))
1704, 169ralrimi 2986 . . 3 (𝜑 → ∀𝑛𝑍𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
171 nfcv 2793 . . . . 5 𝑚(𝐹𝑛)
172 nfmpt1 4780 . . . . . . 7 𝑛(𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
17320, 172nfcxfr 2791 . . . . . 6 𝑛𝐹
174 nfcv 2793 . . . . . 6 𝑛𝑚
175173, 174nffv 6236 . . . . 5 𝑛(𝐹𝑚)
176 fveq2 6229 . . . . 5 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
177171, 175, 176cbvdisj 4662 . . . 4 (Disj 𝑛𝑍 (𝐹𝑛) ↔ Disj 𝑚𝑍 (𝐹𝑚))
178 fveq2 6229 . . . . 5 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
179178disjor 4666 . . . 4 (Disj 𝑚𝑍 (𝐹𝑚) ↔ ∀𝑚𝑍𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅))
180 nfcv 2793 . . . . . 6 𝑛𝑍
181 nfv 1883 . . . . . . 7 𝑛 𝑚 = 𝑘
182 nfcv 2793 . . . . . . . . . 10 𝑛𝑘
183173, 182nffv 6236 . . . . . . . . 9 𝑛(𝐹𝑘)
184175, 183nfin 3853 . . . . . . . 8 𝑛((𝐹𝑚) ∩ (𝐹𝑘))
185 nfcv 2793 . . . . . . . 8 𝑛
186184, 185nfeq 2805 . . . . . . 7 𝑛((𝐹𝑚) ∩ (𝐹𝑘)) = ∅
187181, 186nfor 1874 . . . . . 6 𝑛(𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅)
188180, 187nfral 2974 . . . . 5 𝑛𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅)
189 nfv 1883 . . . . 5 𝑚𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
190 equequ1 1998 . . . . . . 7 (𝑚 = 𝑛 → (𝑚 = 𝑘𝑛 = 𝑘))
191 fveq2 6229 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
192191ineq1d 3846 . . . . . . . 8 (𝑚 = 𝑛 → ((𝐹𝑚) ∩ (𝐹𝑘)) = ((𝐹𝑛) ∩ (𝐹𝑘)))
193192eqeq1d 2653 . . . . . . 7 (𝑚 = 𝑛 → (((𝐹𝑚) ∩ (𝐹𝑘)) = ∅ ↔ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
194190, 193orbi12d 746 . . . . . 6 (𝑚 = 𝑛 → ((𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅) ↔ (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)))
195194ralbidv 3015 . . . . 5 (𝑚 = 𝑛 → (∀𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅) ↔ ∀𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)))
196188, 189, 195cbvral 3197 . . . 4 (∀𝑚𝑍𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅) ↔ ∀𝑛𝑍𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
197177, 179, 1963bitri 286 . . 3 (Disj 𝑛𝑍 (𝐹𝑛) ↔ ∀𝑛𝑍𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
198170, 197sylibr 224 . 2 (𝜑Disj 𝑛𝑍 (𝐹𝑛))
199115, 117, 198jca31 556 1 (𝜑 → ((∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ∧ 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛)) ∧ Disj 𝑛𝑍 (𝐹𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383  w3a 1054   = wceq 1523  wnf 1748  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  cdif 3604  cin 3606  wss 3607  c0 3948   ciun 4552  Disj wdisj 4652   class class class wbr 4685  cmpt 4762  wf 5922  cfv 5926  (class class class)co 6690  cr 9973  1c1 9975   < clt 10112  cle 10113  cmin 10304  cz 11415  cuz 11725  ...cfz 12364  ..^cfzo 12504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505
This theorem is referenced by:  meaiunlelem  41003  meaiuninclem  41015  carageniuncllem2  41057
  Copyright terms: Public domain W3C validator