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 46475
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 4995 . . . . . . . . 9 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
21biimpi 216 . . . . . . . 8 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
32adantl 481 . . . . . . 7 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
4 iundjiun.nph . . . . . . . . 9 𝑛𝜑
5 nfcv 2905 . . . . . . . . . 10 𝑛𝑥
6 nfiu1 5027 . . . . . . . . . 10 𝑛 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)
75, 6nfel 2920 . . . . . . . . 9 𝑛 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)
8 simp2 1138 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑛 ∈ (𝑁...𝑚))
9 simpl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (𝑁...𝑚)) → 𝜑)
10 elfzuz 13560 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ (ℤ𝑁))
11 iundjiun.z . . . . . . . . . . . . . . . . . 18 𝑍 = (ℤ𝑁)
1211eqcomi 2746 . . . . . . . . . . . . . . . . 17 (ℤ𝑁) = 𝑍
1310, 12eleqtrdi 2851 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (𝑁...𝑚) → 𝑛𝑍)
1413adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (𝑁...𝑚)) → 𝑛𝑍)
15 simpr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → 𝑛𝑍)
16 iundjiun.e . . . . . . . . . . . . . . . . . . 19 (𝜑𝐸:𝑍𝑉)
1716ffvelcdmda 7104 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝑍) → (𝐸𝑛) ∈ 𝑉)
1817difexd 5331 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ V)
19 iundjiun.f . . . . . . . . . . . . . . . . . 18 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
2019fvmpt2 7027 . . . . . . . . . . . . . . . . 17 ((𝑛𝑍 ∧ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ V) → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
2115, 18, 20syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
22 difssd 4137 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ⊆ (𝐸𝑛))
2321, 22eqsstrd 4018 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍) → (𝐹𝑛) ⊆ (𝐸𝑛))
249, 14, 23syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (𝑁...𝑚)) → (𝐹𝑛) ⊆ (𝐸𝑛))
25243adant3 1133 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → (𝐹𝑛) ⊆ (𝐸𝑛))
26 simp3 1139 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑥 ∈ (𝐹𝑛))
2725, 26sseldd 3984 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑥 ∈ (𝐸𝑛))
28 rspe 3249 . . . . . . . . . . . 12 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
298, 27, 28syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
30 eliun 4995 . . . . . . . . . . 11 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
3129, 30sylibr 234 . . . . . . . . . 10 ((𝜑𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹𝑛)) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
32313exp 1120 . . . . . . . . 9 (𝜑 → (𝑛 ∈ (𝑁...𝑚) → (𝑥 ∈ (𝐹𝑛) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))))
334, 7, 32rexlimd 3266 . . . . . . . 8 (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)))
3433adantr 480 . . . . . . 7 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)))
353, 34mpd 15 . . . . . 6 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
3635ralrimiva 3146 . . . . 5 (𝜑 → ∀𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
37 dfss3 3972 . . . . 5 ( 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) ⊆ 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ↔ ∀𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
3836, 37sylibr 234 . . . 4 (𝜑 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) ⊆ 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
39 fzssuz 13605 . . . . . . . . 9 (𝑁...𝑚) ⊆ (ℤ𝑁)
4039a1i 11 . . . . . . . 8 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → (𝑁...𝑚) ⊆ (ℤ𝑁))
4130biimpi 216 . . . . . . . 8 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛))
42 nfv 1914 . . . . . . . . 9 𝑛 𝑥 ∈ (𝐸𝑖)
43 fveq2 6906 . . . . . . . . . 10 (𝑛 = 𝑖 → (𝐸𝑛) = (𝐸𝑖))
4443eleq2d 2827 . . . . . . . . 9 (𝑛 = 𝑖 → (𝑥 ∈ (𝐸𝑛) ↔ 𝑥 ∈ (𝐸𝑖)))
4542, 44uzwo4 45058 . . . . . . . 8 (((𝑁...𝑚) ⊆ (ℤ𝑁) ∧ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))))
4640, 41, 45syl2anc 584 . . . . . . 7 (𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))))
4746adantl 481 . . . . . 6 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))))
48 simprl 771 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → 𝑥 ∈ (𝐸𝑛))
49 nfv 1914 . . . . . . . . . . . . . . . . 17 𝑖(𝜑𝑛 ∈ (𝑁...𝑚))
50 nfra1 3284 . . . . . . . . . . . . . . . . 17 𝑖𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))
5149, 50nfan 1899 . . . . . . . . . . . . . . . 16 𝑖((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
52 elfzoelz 13699 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℤ)
5352zred 12722 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℝ)
5453adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℝ)
55 elfzelz 13564 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℤ)
5655zred 12722 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℝ)
5756adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑛 ∈ ℝ)
58 1red 11262 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 1 ∈ ℝ)
5957, 58resubcld 11691 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) ∈ ℝ)
60 elfzolem1 13744 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ≤ (𝑛 − 1))
6160adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ≤ (𝑛 − 1))
6257ltm1d 12200 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑛)
6354, 59, 57, 61, 62lelttrd 11419 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛)
6463ad4ant24 754 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛)
65 simplr 769 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
66 elfzel1 13563 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (𝑁...𝑚) → 𝑁 ∈ ℤ)
6766adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁 ∈ ℤ)
68 elfzel2 13562 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℤ)
6968adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℤ)
7052adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℤ)
71 elfzole1 13707 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (𝑁..^𝑛) → 𝑁𝑖)
7271adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁𝑖)
7369zred 12722 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℝ)
74 1red 11262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (𝑁...𝑚) → 1 ∈ ℝ)
7556, 74resubcld 11691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) ∈ ℝ)
7668zred 12722 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℝ)
7756ltm1d 12200 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑛)
78 elfzle2 13568 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ (𝑁...𝑚) → 𝑛𝑚)
7975, 56, 76, 77, 78ltletrd 11421 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑚)
8079adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑚)
8154, 59, 73, 61, 80lelttrd 11419 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑚)
8254, 73, 81ltled 11409 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖𝑚)
8367, 69, 70, 72, 82elfzd 13555 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚))
8483adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚))
85 rspa 3248 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)) ∧ 𝑖 ∈ (𝑁...𝑚)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
8665, 84, 85syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
8786adantlll 718 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))
8864, 87mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ¬ 𝑥 ∈ (𝐸𝑖))
8988ex 412 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → (𝑖 ∈ (𝑁..^𝑛) → ¬ 𝑥 ∈ (𝐸𝑖)))
9051, 89ralrimi 3257 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ∀𝑖 ∈ (𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸𝑖))
91 ralnex 3072 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸𝑖) ↔ ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸𝑖))
9290, 91sylib 218 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸𝑖))
93 eliun 4995 . . . . . . . . . . . . . 14 (𝑥 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖) ↔ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸𝑖))
9492, 93sylnibr 329 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ¬ 𝑥 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖))
9594adantrl 716 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → ¬ 𝑥 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖))
9648, 95eldifd 3962 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → 𝑥 ∈ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
9714, 21syldan 591 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑁...𝑚)) → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
9897eqcomd 2743 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑁...𝑚)) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) = (𝐹𝑛))
9998adantr 480 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) = (𝐹𝑛))
10096, 99eleqtrd 2843 . . . . . . . . . 10 (((𝜑𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖)))) → 𝑥 ∈ (𝐹𝑛))
101100ex 412 . . . . . . . . 9 ((𝜑𝑛 ∈ (𝑁...𝑚)) → ((𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → 𝑥 ∈ (𝐹𝑛)))
102101ex 412 . . . . . . . 8 (𝜑 → (𝑛 ∈ (𝑁...𝑚) → ((𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → 𝑥 ∈ (𝐹𝑛))))
1034, 102reximdai 3261 . . . . . . 7 (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛)))
104103adantr 480 . . . . . 6 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛)))
10547, 104mpd 15 . . . . 5 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹𝑛))
106105, 1sylibr 234 . . . 4 ((𝜑𝑥 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛)) → 𝑥 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛))
10738, 106eqelssd 4005 . . 3 (𝜑 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
108107ralrimivw 3150 . 2 (𝜑 → ∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
10911iuneqfzuz 45346 . . 3 (∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) → 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛))
110108, 109syl 17 . 2 (𝜑 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛))
111 fveq2 6906 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → (𝐸𝑛) = (𝐸𝑚))
112 oveq2 7439 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝑁..^𝑛) = (𝑁..^𝑚))
113112iuneq1d 5019 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖))
114111, 113difeq12d 4127 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) = ((𝐸𝑚) ∖ 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖)))
115114cbvmptv 5255 . . . . . . . . . . . 12 (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖))) = (𝑚𝑍 ↦ ((𝐸𝑚) ∖ 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖)))
11619, 115eqtri 2765 . . . . . . . . . . 11 𝐹 = (𝑚𝑍 ↦ ((𝐸𝑚) ∖ 𝑖 ∈ (𝑁..^𝑚)(𝐸𝑖)))
117 simpllr 776 . . . . . . . . . . 11 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → 𝑛𝑍)
118 simplr 769 . . . . . . . . . . 11 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → 𝑘𝑍)
119 simpr 484 . . . . . . . . . . 11 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → 𝑛 < 𝑘)
12011, 116, 117, 118, 119iundjiunlem 46474 . . . . . . . . . 10 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑛 < 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
121120adantlr 715 . . . . . . . . 9 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ 𝑛 < 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
122 simpll 767 . . . . . . . . . 10 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝜑𝑛𝑍) ∧ 𝑘𝑍))
123 neqne 2948 . . . . . . . . . . . 12 𝑛 = 𝑘𝑛𝑘)
124 id 22 . . . . . . . . . . . . . . . . . 18 (𝑘𝑍𝑘𝑍)
125124, 11eleqtrdi 2851 . . . . . . . . . . . . . . . . 17 (𝑘𝑍𝑘 ∈ (ℤ𝑁))
126 eluzelz 12888 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ𝑁) → 𝑘 ∈ ℤ)
127125, 126syl 17 . . . . . . . . . . . . . . . 16 (𝑘𝑍𝑘 ∈ ℤ)
128127zred 12722 . . . . . . . . . . . . . . 15 (𝑘𝑍𝑘 ∈ ℝ)
129128adantl 481 . . . . . . . . . . . . . 14 ((𝑛𝑍𝑘𝑍) → 𝑘 ∈ ℝ)
130129ad2antrr 726 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ)
131 id 22 . . . . . . . . . . . . . . . . 17 (𝑛𝑍𝑛𝑍)
132131, 11eleqtrdi 2851 . . . . . . . . . . . . . . . 16 (𝑛𝑍𝑛 ∈ (ℤ𝑁))
133 eluzelz 12888 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ𝑁) → 𝑛 ∈ ℤ)
134132, 133syl 17 . . . . . . . . . . . . . . 15 (𝑛𝑍𝑛 ∈ ℤ)
135134zred 12722 . . . . . . . . . . . . . 14 (𝑛𝑍𝑛 ∈ ℝ)
136135ad3antrrr 730 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ)
137 simpr 484 . . . . . . . . . . . . . . 15 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → ¬ 𝑛 < 𝑘)
138129adantr 480 . . . . . . . . . . . . . . . 16 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ)
139135ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ)
140138, 139lenltd 11407 . . . . . . . . . . . . . . 15 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → (𝑘𝑛 ↔ ¬ 𝑛 < 𝑘))
141137, 140mpbird 257 . . . . . . . . . . . . . 14 (((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘𝑛)
142141adantlr 715 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘𝑛)
143 simplr 769 . . . . . . . . . . . . 13 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛𝑘)
144130, 136, 142, 143leneltd 11415 . . . . . . . . . . . 12 ((((𝑛𝑍𝑘𝑍) ∧ 𝑛𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛)
145123, 144sylanl2 681 . . . . . . . . . . 11 ((((𝑛𝑍𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛)
146145ad5ant2345 1372 . . . . . . . . . 10 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛)
147 anass 468 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑘𝑍) ↔ (𝜑 ∧ (𝑛𝑍𝑘𝑍)))
148 incom 4209 . . . . . . . . . . . . 13 ((𝐹𝑛) ∩ (𝐹𝑘)) = ((𝐹𝑘) ∩ (𝐹𝑛))
149148a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ((𝐹𝑘) ∩ (𝐹𝑛)))
150 simplrr 778 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → 𝑘𝑍)
151 simplrl 777 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → 𝑛𝑍)
152 simpr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → 𝑘 < 𝑛)
15311, 116, 150, 151, 152iundjiunlem 46474 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹𝑘) ∩ (𝐹𝑛)) = ∅)
154149, 153eqtrd 2777 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛𝑍𝑘𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
155147, 154sylanb 581 . . . . . . . . . 10 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ 𝑘 < 𝑛) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
156122, 146, 155syl2anc 584 . . . . . . . . 9 (((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
157121, 156pm2.61dan 813 . . . . . . . 8 ((((𝜑𝑛𝑍) ∧ 𝑘𝑍) ∧ ¬ 𝑛 = 𝑘) → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
158157ex 412 . . . . . . 7 (((𝜑𝑛𝑍) ∧ 𝑘𝑍) → (¬ 𝑛 = 𝑘 → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
159 df-or 849 . . . . . . 7 ((𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅) ↔ (¬ 𝑛 = 𝑘 → ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
160158, 159sylibr 234 . . . . . 6 (((𝜑𝑛𝑍) ∧ 𝑘𝑍) → (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
161160ralrimiva 3146 . . . . 5 ((𝜑𝑛𝑍) → ∀𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
162161ex 412 . . . 4 (𝜑 → (𝑛𝑍 → ∀𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)))
1634, 162ralrimi 3257 . . 3 (𝜑 → ∀𝑛𝑍𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
164 nfcv 2905 . . . . 5 𝑚(𝐹𝑛)
165 nfmpt1 5250 . . . . . . 7 𝑛(𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
16619, 165nfcxfr 2903 . . . . . 6 𝑛𝐹
167 nfcv 2905 . . . . . 6 𝑛𝑚
168166, 167nffv 6916 . . . . 5 𝑛(𝐹𝑚)
169 fveq2 6906 . . . . 5 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
170164, 168, 169cbvdisj 5120 . . . 4 (Disj 𝑛𝑍 (𝐹𝑛) ↔ Disj 𝑚𝑍 (𝐹𝑚))
171 fveq2 6906 . . . . 5 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
172171disjor 5125 . . . 4 (Disj 𝑚𝑍 (𝐹𝑚) ↔ ∀𝑚𝑍𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅))
173 nfcv 2905 . . . . . 6 𝑛𝑍
174 nfv 1914 . . . . . . 7 𝑛 𝑚 = 𝑘
175 nfcv 2905 . . . . . . . . . 10 𝑛𝑘
176166, 175nffv 6916 . . . . . . . . 9 𝑛(𝐹𝑘)
177168, 176nfin 4224 . . . . . . . 8 𝑛((𝐹𝑚) ∩ (𝐹𝑘))
178 nfcv 2905 . . . . . . . 8 𝑛
179177, 178nfeq 2919 . . . . . . 7 𝑛((𝐹𝑚) ∩ (𝐹𝑘)) = ∅
180174, 179nfor 1904 . . . . . 6 𝑛(𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅)
181173, 180nfralw 3311 . . . . 5 𝑛𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅)
182 nfv 1914 . . . . 5 𝑚𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)
183 equequ1 2024 . . . . . . 7 (𝑚 = 𝑛 → (𝑚 = 𝑘𝑛 = 𝑘))
184 fveq2 6906 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
185184ineq1d 4219 . . . . . . . 8 (𝑚 = 𝑛 → ((𝐹𝑚) ∩ (𝐹𝑘)) = ((𝐹𝑛) ∩ (𝐹𝑘)))
186185eqeq1d 2739 . . . . . . 7 (𝑚 = 𝑛 → (((𝐹𝑚) ∩ (𝐹𝑘)) = ∅ ↔ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
187183, 186orbi12d 919 . . . . . 6 (𝑚 = 𝑛 → ((𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅) ↔ (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)))
188187ralbidv 3178 . . . . 5 (𝑚 = 𝑛 → (∀𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅) ↔ ∀𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅)))
189181, 182, 188cbvralw 3306 . . . 4 (∀𝑚𝑍𝑘𝑍 (𝑚 = 𝑘 ∨ ((𝐹𝑚) ∩ (𝐹𝑘)) = ∅) ↔ ∀𝑛𝑍𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
190170, 172, 1893bitri 297 . . 3 (Disj 𝑛𝑍 (𝐹𝑛) ↔ ∀𝑛𝑍𝑘𝑍 (𝑛 = 𝑘 ∨ ((𝐹𝑛) ∩ (𝐹𝑘)) = ∅))
191163, 190sylibr 234 . 2 (𝜑Disj 𝑛𝑍 (𝐹𝑛))
192108, 110, 191jca31 514 1 (𝜑 → ((∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ∧ 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛)) ∧ Disj 𝑛𝑍 (𝐹𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 848  w3a 1087   = wceq 1540  wnf 1783  wcel 2108  wne 2940  wral 3061  wrex 3070  Vcvv 3480  cdif 3948  cin 3950  wss 3951  c0 4333   ciun 4991  Disj wdisj 5110   class class class wbr 5143  cmpt 5225  wf 6557  cfv 6561  (class class class)co 7431  cr 11154  1c1 11156   < clt 11295  cle 11296  cmin 11492  cz 12613  cuz 12878  ...cfz 13547  ..^cfzo 13694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-fzo 13695
This theorem is referenced by:  meaiunlelem  46483  meaiuninclem  46495  carageniuncllem2  46537
  Copyright terms: Public domain W3C validator