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 42623
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 4916 . . . . . . . . 9 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
21biimpi 217 . . . . . . . 8 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
32adantl 482 . . . . . . 7 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
4 iundjiun.nph . . . . . . . . 9 𝑛𝜑
5 nfcv 2977 . . . . . . . . . 10 𝑛𝑥
6 nfiu1 4945 . . . . . . . . . 10 𝑛 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)
75, 6nfel 2992 . . . . . . . . 9 𝑛 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)
8 simp2 1129 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑛 ∈ (𝑁...𝑚))
9 simpl 483 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (𝑁...𝑚)) → 𝜑)
10 elfzuz 12894 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ (ℤ𝑁))
11 iundjiun.z . . . . . . . . . . . . . . . . . 18 𝑍 = (ℤ𝑁)
1211eqcomi 2830 . . . . . . . . . . . . . . . . 17 (ℤ𝑁) = 𝑍
1310, 12eleqtrdi 2923 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (𝑁...𝑚) → 𝑛𝑍)
1413adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (𝑁...𝑚)) → 𝑛𝑍)
15 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → 𝑛𝑍)
16 iundjiun.e . . . . . . . . . . . . . . . . . . 19 (𝜑𝐸:𝑍𝑉)
1716ffvelrnda 6844 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝑍) → (𝐸𝑛) ∈ 𝑉)
18 difexg 5223 . . . . . . . . . . . . . . . . . 18 ((𝐸𝑛) ∈ 𝑉 → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ V)
1917, 18syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ V)
20 iundjiun.f . . . . . . . . . . . . . . . . . 18 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
2120fvmpt2 6772 . . . . . . . . . . . . . . . . 17 ((𝑛𝑍 ∧ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ V) → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
2215, 19, 21syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
23 difssd 4108 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ⊆ (𝐸𝑛))
2422, 23eqsstrd 4004 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍) → (𝐹𝑛) ⊆ (𝐸𝑛))
259, 14, 24syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (𝑁...𝑚)) → (𝐹𝑛) ⊆ (𝐸𝑛))
26253adant3 1124 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → (𝐹𝑛) ⊆ (𝐸𝑛))
27 simp3 1130 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑥 ∈ (𝐹𝑛))
2826, 27sseldd 3967 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑥 ∈ (𝐸𝑛))
29 rspe 3304 . . . . . . . . . . . 12 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
308, 28, 29syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
31 eliun 4916 . . . . . . . . . . 11 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
3230, 31sylibr 235 . . . . . . . . . 10 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
33323exp 1111 . . . . . . . . 9 (𝜑 → (𝑛 ∈ (𝑁...𝑚) → (𝑥 ∈ (𝐹𝑛) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))))
344, 7, 33rexlimd 3317 . . . . . . . 8 (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)))
3534adantr 481 . . . . . . 7 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)))
363, 35mpd 15 . . . . . 6 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
3736ralrimiva 3182 . . . . 5 (𝜑 → ∀𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
38 dfss3 3955 . . . . 5 ( 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) ⊆ 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ↔ ∀𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
3937, 38sylibr 235 . . . 4 (𝜑 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) ⊆ 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
40 fzssuz 12938 . . . . . . . . 9 (𝑁...𝑚) ⊆ (ℤ𝑁)
4140a1i 11 . . . . . . . 8 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → (𝑁...𝑚) ⊆ (ℤ𝑁))
4231biimpi 217 . . . . . . . 8 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
43 nfv 1906 . . . . . . . . 9 𝑛 𝑥 ∈ (𝐸𝑖)
44 fveq2 6664 . . . . . . . . . 10 (𝑛 = 𝑖 → (𝐸𝑛) = (𝐸𝑖))
4544eleq2d 2898 . . . . . . . . 9 (𝑛 = 𝑖 → (𝑥 ∈ (𝐸𝑛) ↔ 𝑥 ∈ (𝐸𝑖)))
4643, 45uzwo4 41195 . . . . . . . 8 (((𝑁...𝑚) ⊆ (ℤ𝑁) ∧ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))))
4741, 42, 46syl2anc 584 . . . . . . 7 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))))
4847adantl 482 . . . . . 6 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))))
49 simprl 767 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → 𝑥 ∈ (𝐸𝑛))
50 nfv 1906 . . . . . . . . . . . . . . . . 17 𝑖(𝜑𝑛 ∈ (𝑁...𝑚))
51 nfra1 3219 . . . . . . . . . . . . . . . . 17 𝑖𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))
5250, 51nfan 1891 . . . . . . . . . . . . . . . 16 𝑖((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
53 elfzoelz 13028 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℤ)
5453zred 12076 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℝ)
5554adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℝ)
56 elfzelz 12898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℤ)
5756zred 12076 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℝ)
5857adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑛 ∈ ℝ)
59 1red 10631 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 1 ∈ ℝ)
6058, 59resubcld 11057 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) ∈ ℝ)
61 elfzolem1 41469 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ≤ (𝑛 − 1))
6261adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ≤ (𝑛 − 1))
6358ltm1d 11561 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑛)
6455, 60, 58, 62, 63lelttrd 10787 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛)
6564ad4ant24 750 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛)
66 simplr 765 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
67 elfzel1 12897 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (𝑁...𝑚) → 𝑁 ∈ ℤ)
6867adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁 ∈ ℤ)
69 elfzel2 12896 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℤ)
7069adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℤ)
7153adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℤ)
7268, 70, 713jca 1120 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ))
73 elfzole1 13036 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (𝑁..^𝑛) → 𝑁𝑖)
7473adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁𝑖)
7570zred 12076 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℝ)
76 1red 10631 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (𝑁...𝑚) → 1 ∈ ℝ)
7757, 76resubcld 11057 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) ∈ ℝ)
7869zred 12076 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℝ)
7957ltm1d 11561 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑛)
80 elfzle2 12901 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (𝑁...𝑚) → 𝑛𝑚)
8177, 57, 78, 79, 80ltletrd 10789 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑚)
8281adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑚)
8355, 60, 75, 62, 82lelttrd 10787 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑚)
8455, 75, 83ltled 10777 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖𝑚)
8572, 74, 84jca32 516 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑁𝑖𝑖𝑚)))
86 elfz2 12889 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑁...𝑚) ↔ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑁𝑖𝑖𝑚)))
8785, 86sylibr 235 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚))
8887adantlr 711 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚))
89 rspa 3206 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)) ∧ 𝑖 ∈ (𝑁...𝑚)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
9066, 88, 89syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
9190adantlll 714 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
9265, 91mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ¬ 𝑥 ∈ (𝐸𝑖))
9392ex 413 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → (𝑖 ∈ (𝑁..^𝑛) → ¬ 𝑥 ∈ (𝐸𝑖)))
9452, 93ralrimi 3216 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ∀𝑖 ∈ (𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸𝑖))
95 ralnex 3236 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸𝑖) ↔ ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸𝑖))
9694, 95sylib 219 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸𝑖))
97 eliun 4916 . . . . . . . . . . . . . 14 (𝑥 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖) ↔ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸𝑖))
9896, 97sylnibr 330 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ¬ 𝑥 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖))
9998adantrl 712 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → ¬ 𝑥 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖))
10049, 99eldifd 3946 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → 𝑥 ∈ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
10114, 22syldan 591 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑁...𝑚)) → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
102101eqcomd 2827 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑁...𝑚)) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) = (𝐹𝑛))
103102adantr 481 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) = (𝐹𝑛))
104100, 103eleqtrd 2915 . . . . . . . . . 10 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → 𝑥 ∈ (𝐹𝑛))
105104ex 413 . . . . . . . . 9 ((𝜑𝑛 ∈ (𝑁...𝑚)) → ((𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → 𝑥 ∈ (𝐹𝑛)))
106105ex 413 . . . . . . . 8 (𝜑 → (𝑛 ∈ (𝑁...𝑚) → ((𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → 𝑥 ∈ (𝐹𝑛))))
1074, 106reximdai 3311 . . . . . . 7 (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛)))
108107adantr 481 . . . . . 6 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛)))
10948, 108mpd 15 . . . . 5 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
110109, 1sylibr 235 . . . 4 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛))
11139, 110eqelssd 3987 . . 3 (𝜑 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
112111ralrimivw 3183 . 2 (𝜑 → ∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
11311iuneqfzuz 41483 . . 3 (∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛))
114112, 113syl 17 . 2 (𝜑 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛))
115 fveq2 6664 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → (𝐸𝑛) = (𝐸𝑚))
116 oveq2 7153 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝑁..^𝑛) = (𝑁..^𝑚))
117116iuneq1d 4938 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖))
118115, 117difeq12d 4099 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) = ((𝐸𝑚) ∖ 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖)))
119118cbvmptv 5161 . . . . . . . . . . . 12 (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖))) = (𝑚𝑍 ↦ ((𝐸𝑚) ∖ 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖)))
12020, 119eqtri 2844 . . . . . . . . . . 11 𝐹 = (𝑚𝑍 ↦ ((𝐸𝑚) ∖ 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖)))
121 simpllr 772 . . . . . . . . . . 11 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → 𝑛𝑍)
122 simplr 765 . . . . . . . . . . 11 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → 𝑘𝑍)
123 simpr 485 . . . . . . . . . . 11 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → 𝑛 < 𝑘)
12411, 120, 121, 122, 123iundjiunlem 42622 . . . . . . . . . 10 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
125124adantlr 711 . . . . . . . . 9 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ 𝑛 < 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
126 simpll 763 . . . . . . . . . 10 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝜑𝑛𝑍) ∧ 𝑘𝑍))
127 neqne 3024 . . . . . . . . . . . 12 𝑛 = 𝑘𝑛𝑘)
128 id 22 . . . . . . . . . . . . . . . . . 18 (𝑘𝑍𝑘𝑍)
129128, 11eleqtrdi 2923 . . . . . . . . . . . . . . . . 17 (𝑘𝑍𝑘 ∈ (ℤ𝑁))
130 eluzelz 12242 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ𝑁) → 𝑘 ∈ ℤ)
131129, 130syl 17 . . . . . . . . . . . . . . . 16 (𝑘𝑍𝑘 ∈ ℤ)
132131zred 12076 . . . . . . . . . . . . . . 15 (𝑘𝑍𝑘 ∈ ℝ)
133132adantl 482 . . . . . . . . . . . . . 14 ((𝑛𝑍𝑘𝑍) → 𝑘 ∈ ℝ)
134133ad2antrr 722 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ)
135 id 22 . . . . . . . . . . . . . . . . 17 (𝑛𝑍𝑛𝑍)
136135, 11eleqtrdi 2923 . . . . . . . . . . . . . . . 16 (𝑛𝑍𝑛 ∈ (ℤ𝑁))
137 eluzelz 12242 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ𝑁) → 𝑛 ∈ ℤ)
138136, 137syl 17 . . . . . . . . . . . . . . 15 (𝑛𝑍𝑛 ∈ ℤ)
139138zred 12076 . . . . . . . . . . . . . 14 (𝑛𝑍𝑛 ∈ ℝ)
140139ad3antrrr 726 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ)
141 simpr 485 . . . . . . . . . . . . . . 15 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → ¬ 𝑛 < 𝑘)
142133adantr 481 . . . . . . . . . . . . . . . 16 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ)
143139ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ)
144142, 143lenltd 10775 . . . . . . . . . . . . . . 15 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → (𝑘𝑛 ↔ ¬ 𝑛 < 𝑘))
145141, 144mpbird 258 . . . . . . . . . . . . . 14 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘𝑛)
146145adantlr 711 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘𝑛)
147 simplr 765 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛𝑘)
148134, 140, 146, 147leneltd 10783 . . . . . . . . . . . 12 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛)
149127, 148sylanl2 677 . . . . . . . . . . 11 ((((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛)
150149ad5ant2345 1362 . . . . . . . . . 10 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛)
151 anass 469 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑘𝑍) ↔ (𝜑 ∧ (𝑛𝑍𝑘𝑍)))
152 incom 4177 . . . . . . . . . . . . 13 ((𝐹𝑛) ∩ (𝐹𝑘)) = ((𝐹𝑘) ∩ (𝐹𝑛))
153152a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ((𝐹𝑘) ∩ (𝐹𝑛)))
154 simplrr 774 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → 𝑘𝑍)
155 simplrl 773 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → 𝑛𝑍)
156 simpr 485 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → 𝑘 < 𝑛)
15711, 120, 154, 155, 156iundjiunlem 42622 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹𝑘) ∩ (𝐹𝑛)) = ∅)
158153, 157eqtrd 2856 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
159151, 158sylanb 581 . . . . . . . . . 10 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑘 < 𝑛) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
160126, 150, 159syl2anc 584 . . . . . . . . 9 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
161125, 160pm2.61dan 809 . . . . . . . 8 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
162161ex 413 . . . . . . 7 (((𝜑𝑛𝑍) ∧ 𝑘𝑍) → (¬ 𝑛 = 𝑘 → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
163 df-or 842 . . . . . . 7 ((𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅) ↔ (¬ 𝑛 = 𝑘 → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
164162, 163sylibr 235 . . . . . 6 (((𝜑𝑛𝑍) ∧ 𝑘𝑍) → (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
165164ralrimiva 3182 . . . . 5 ((𝜑𝑛𝑍) → ∀𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
166165ex 413 . . . 4 (𝜑 → (𝑛𝑍 → ∀𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)))
1674, 166ralrimi 3216 . . 3 (𝜑 → ∀𝑛𝑍𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
168 nfcv 2977 . . . . 5 𝑚(𝐹𝑛)
169 nfmpt1 5156 . . . . . . 7 𝑛(𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
17020, 169nfcxfr 2975 . . . . . 6 𝑛𝐹
171 nfcv 2977 . . . . . 6 𝑛𝑚
172170, 171nffv 6674 . . . . 5 𝑛(𝐹𝑚)
173 fveq2 6664 . . . . 5 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
174168, 172, 173cbvdisj 5033 . . . 4 (Disj 𝑛𝑍 (𝐹𝑛) ↔ Disj 𝑚𝑍 (𝐹𝑚))
175 fveq2 6664 . . . . 5 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
176175disjor 5038 . . . 4 (Disj 𝑚𝑍 (𝐹𝑚) ↔ ∀𝑚𝑍𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅))
177 nfcv 2977 . . . . . 6 𝑛𝑍
178 nfv 1906 . . . . . . 7 𝑛 𝑚 = 𝑘
179 nfcv 2977 . . . . . . . . . 10 𝑛𝑘
180170, 179nffv 6674 . . . . . . . . 9 𝑛(𝐹𝑘)
181172, 180nfin 4192 . . . . . . . 8 𝑛((𝐹𝑚) ∩ (𝐹𝑘))
182 nfcv 2977 . . . . . . . 8 𝑛
183181, 182nfeq 2991 . . . . . . 7 𝑛((𝐹𝑚) ∩ (𝐹𝑘)) = ∅
184178, 183nfor 1896 . . . . . 6 𝑛(𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅)
185177, 184nfral 3226 . . . . 5 𝑛𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅)
186 nfv 1906 . . . . 5 𝑚𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
187 equequ1 2023 . . . . . . 7 (𝑚 = 𝑛 → (𝑚 = 𝑘𝑛 = 𝑘))
188 fveq2 6664 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
189188ineq1d 4187 . . . . . . . 8 (𝑚 = 𝑛 → ((𝐹𝑚) ∩ (𝐹𝑘)) = ((𝐹𝑛) ∩ (𝐹𝑘)))
190189eqeq1d 2823 . . . . . . 7 (𝑚 = 𝑛 → (((𝐹𝑚) ∩ (𝐹𝑘)) = ∅ ↔ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
191187, 190orbi12d 912 . . . . . 6 (𝑚 = 𝑛 → ((𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅) ↔ (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)))
192191ralbidv 3197 . . . . 5 (𝑚 = 𝑛 → (∀𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅) ↔ ∀𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)))
193185, 186, 192cbvral 3446 . . . 4 (∀𝑚𝑍𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅) ↔ ∀𝑛𝑍𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
194174, 176, 1933bitri 298 . . 3 (Disj 𝑛𝑍 (𝐹𝑛) ↔ ∀𝑛𝑍𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
195167, 194sylibr 235 . 2 (𝜑Disj 𝑛𝑍 (𝐹𝑛))
196112, 114, 195jca31 515 1 (𝜑 → ((∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ∧ 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛)) ∧ Disj 𝑛𝑍 (𝐹𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 841  w3a 1079   = wceq 1528  wnf 1775  wcel 2105  wne 3016  wral 3138  wrex 3139  Vcvv 3495  cdif 3932  cin 3934  wss 3935  c0 4290   ciun 4912  Disj wdisj 5023   class class class wbr 5058  cmpt 5138  wf 6345  cfv 6349  (class class class)co 7145  cr 10525  1c1 10527   < clt 10664  cle 10665  cmin 10859  cz 11970  cuz 12232  ...cfz 12882  ..^cfzo 13023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-13 2383  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-disj 5024  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-n0 11887  df-z 11971  df-uz 12233  df-fz 12883  df-fzo 13024
This theorem is referenced by:  meaiunlelem  42631  meaiuninclem  42643  carageniuncllem2  42685
  Copyright terms: Public domain W3C validator