Metamath Proof Explorer

Theorem iundjiun

Description: Given a sequence E of sets, a sequence F 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)

Ref Expression
Hypotheses iundjiun.nph ⊢ Ⅎ 𝑛 𝜑
iundjiun.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
iundjiun.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝑉 )
iundjiun.f ⊢ 𝐹 = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
Assertion iundjiun ( 𝜑 → ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ∧ ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∧ Disj 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 iundjiun.nph ⊢ Ⅎ 𝑛 𝜑
2 iundjiun.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
3 iundjiun.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝑉 )
4 iundjiun.f ⊢ 𝐹 = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
5 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) )
6 5 biimpi ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) )
8 nfcv ⊢ Ⅎ 𝑛 𝑥
9 nfiu1 ⊢ Ⅎ 𝑛 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 )
10 8 9 nfel ⊢ Ⅎ 𝑛 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 )
11 simp2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝑛 ∈ ( 𝑁 ... 𝑚 ) )
12 simpl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) → 𝜑 )
13 elfzuz ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) )
14 2 eqcomi ⊢ ( ℤ≥ ‘ 𝑁 ) = 𝑍
15 13 14 eleqtrdi ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → 𝑛 ∈ 𝑍 )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) → 𝑛 ∈ 𝑍 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
18 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ∈ 𝑉 )
19 18 difexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ∈ V )
20 4 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ∈ V ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
21 17 19 20 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
22 difssd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ⊆ ( 𝐸 ‘ 𝑛 ) )
23 21 22 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ 𝑛 ) )
24 12 16 23 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ 𝑛 ) )
25 24 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ 𝑛 ) )
26 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) )
27 25 26 sseldd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) )
28 rspe ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) )
29 11 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) )
30 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) )
31 29 30 sylibr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) )
32 31 3exp ⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → ( 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) → 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ) ) )
33 1 10 32 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) → 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) ) → ( ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) → 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ) )
35 7 34 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) )
36 35 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) )
37 dfss3 ⊢ ( ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ↔ ∀ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) )
38 36 37 sylibr ⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) )
39 fzssuz ⊢ ( 𝑁 ... 𝑚 ) ⊆ ( ℤ≥ ‘ 𝑁 )
40 39 a1i ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) → ( 𝑁 ... 𝑚 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
41 30 biimpi ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) )
42 nfv ⊢ Ⅎ 𝑛 𝑥 ∈ ( 𝐸 ‘ 𝑖 )
43 fveq2 ⊢ ( 𝑛 = 𝑖 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑖 ) )
44 43 eleq2d ⊢ ( 𝑛 = 𝑖 → ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↔ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) )
45 42 44 uzwo4 ⊢ ( ( ( 𝑁 ... 𝑚 ) ⊆ ( ℤ≥ ‘ 𝑁 ) ∧ ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
46 40 41 45 syl2anc ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
48 simprl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) → 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) )
49 nfv ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) )
50 nfra1 ⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) )
51 49 50 nfan ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) )
52 elfzoelz ⊢ ( 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) → 𝑖 ∈ ℤ )
53 52 zred ⊢ ( 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) → 𝑖 ∈ ℝ )
54 53 adantl ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑖 ∈ ℝ )
55 elfzelz ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → 𝑛 ∈ ℤ )
56 55 zred ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → 𝑛 ∈ ℝ )
57 56 adantr ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑛 ∈ ℝ )
58 1red ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 1 ∈ ℝ )
59 57 58 resubcld ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ( 𝑛 − 1 ) ∈ ℝ )
60 elfzolem1 ⊢ ( 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) → 𝑖 ≤ ( 𝑛 − 1 ) )
61 60 adantl ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑖 ≤ ( 𝑛 − 1 ) )
62 57 ltm1d ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ( 𝑛 − 1 ) < 𝑛 )
63 54 59 57 61 62 lelttrd ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑖 < 𝑛 )
64 63 ad4ant24 ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑖 < 𝑛 )
65 simplr ⊢ ( ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) )
66 elfzel1 ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → 𝑁 ∈ ℤ )
67 66 adantr ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑁 ∈ ℤ )
68 elfzel2 ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → 𝑚 ∈ ℤ )
69 68 adantr ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑚 ∈ ℤ )
70 52 adantl ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑖 ∈ ℤ )
71 elfzole1 ⊢ ( 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) → 𝑁 ≤ 𝑖 )
72 71 adantl ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑁 ≤ 𝑖 )
73 69 zred ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑚 ∈ ℝ )
74 1red ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → 1 ∈ ℝ )
75 56 74 resubcld ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → ( 𝑛 − 1 ) ∈ ℝ )
76 68 zred ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → 𝑚 ∈ ℝ )
77 56 ltm1d ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → ( 𝑛 − 1 ) < 𝑛 )
78 elfzle2 ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → 𝑛 ≤ 𝑚 )
79 75 56 76 77 78 ltletrd ⊢ ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → ( 𝑛 − 1 ) < 𝑚 )
80 79 adantr ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ( 𝑛 − 1 ) < 𝑚 )
81 54 59 73 61 80 lelttrd ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑖 < 𝑚 )
82 54 73 81 ltled ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑖 ≤ 𝑚 )
83 67 69 70 72 82 elfzd ⊢ ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑖 ∈ ( 𝑁 ... 𝑚 ) )
84 83 adantlr ⊢ ( ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑖 ∈ ( 𝑁 ... 𝑚 ) )
85 rspa ⊢ ( ( ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ) → ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) )
86 65 84 85 syl2anc ⊢ ( ( ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) )
87 86 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) )
88 64 87 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) )
89 88 ex ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) → ( 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) )
90 51 89 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) )
91 ralnex ⊢ ( ∀ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ↔ ¬ ∃ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) )
92 90 91 sylib ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) → ¬ ∃ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) )
93 eliun ⊢ ( 𝑥 ∈ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) )
94 92 93 sylnibr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) → ¬ 𝑥 ∈ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) )
95 94 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) → ¬ 𝑥 ∈ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) )
96 48 95 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) → 𝑥 ∈ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
97 16 21 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
98 97 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) = ( 𝐹 ‘ 𝑛 ) )
99 98 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) = ( 𝐹 ‘ 𝑛 ) )
100 96 99 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) → 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) )
101 100 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ) → ( ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) → 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) )
102 101 ex ⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝑁 ... 𝑚 ) → ( ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) → 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) ) )
103 1 102 reximdai ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) )
104 103 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ) → ( ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ∧ ∀ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝑖 < 𝑛 → ¬ 𝑥 ∈ ( 𝐸 ‘ 𝑖 ) ) ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) )
105 47 104 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) )
106 105 5 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) )
107 38 106 eqelssd ⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) )
108 107 ralrimivw ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) )
109 2 iuneqfzuz ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) → ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
110 108 109 syl ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
111 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑚 ) )
112 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑁 ..^ 𝑛 ) = ( 𝑁 ..^ 𝑚 ) )
113 112 iuneq1d ⊢ ( 𝑛 = 𝑚 → ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) )
114 111 113 difeq12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) ) )
115 114 cbvmptv ⊢ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) ) )
116 4 115 eqtri ⊢ 𝐹 = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) ) )
117 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 < 𝑘 ) → 𝑛 ∈ 𝑍 )
118 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 < 𝑘 ) → 𝑘 ∈ 𝑍 )
119 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 < 𝑘 ) → 𝑛 < 𝑘 )
120 2 116 117 118 119 iundjiunlem ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 < 𝑘 ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ )
121 120 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ 𝑛 = 𝑘 ) ∧ 𝑛 < 𝑘 ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ )
122 simpll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ 𝑛 = 𝑘 ) ∧ ¬ 𝑛 < 𝑘 ) → ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) )
123 neqne ⊢ ( ¬ 𝑛 = 𝑘 → 𝑛 ≠ 𝑘 )
124 id ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ 𝑍 )
125 124 2 eleqtrdi ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
126 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑘 ∈ ℤ )
127 125 126 syl ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
128 127 zred ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℝ )
129 128 adantl ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℝ )
130 129 ad2antrr ⊢ ( ( ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 ≠ 𝑘 ) ∧ ¬ 𝑛 < 𝑘 ) → 𝑘 ∈ ℝ )
131 id ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍 )
132 131 2 eleqtrdi ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) )
133 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑛 ∈ ℤ )
134 132 133 syl ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
135 134 zred ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℝ )
136 135 ad3antrrr ⊢ ( ( ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 ≠ 𝑘 ) ∧ ¬ 𝑛 < 𝑘 ) → 𝑛 ∈ ℝ )
137 simpr ⊢ ( ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ 𝑛 < 𝑘 ) → ¬ 𝑛 < 𝑘 )
138 129 adantr ⊢ ( ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ 𝑛 < 𝑘 ) → 𝑘 ∈ ℝ )
139 135 ad2antrr ⊢ ( ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ 𝑛 < 𝑘 ) → 𝑛 ∈ ℝ )
140 138 139 lenltd ⊢ ( ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ 𝑛 < 𝑘 ) → ( 𝑘 ≤ 𝑛 ↔ ¬ 𝑛 < 𝑘 ) )
141 137 140 mpbird ⊢ ( ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ 𝑛 < 𝑘 ) → 𝑘 ≤ 𝑛 )
142 141 adantlr ⊢ ( ( ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 ≠ 𝑘 ) ∧ ¬ 𝑛 < 𝑘 ) → 𝑘 ≤ 𝑛 )
143 simplr ⊢ ( ( ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 ≠ 𝑘 ) ∧ ¬ 𝑛 < 𝑘 ) → 𝑛 ≠ 𝑘 )
144 130 136 142 143 leneltd ⊢ ( ( ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 ≠ 𝑘 ) ∧ ¬ 𝑛 < 𝑘 ) → 𝑘 < 𝑛 )
145 123 144 sylanl2 ⊢ ( ( ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ 𝑛 = 𝑘 ) ∧ ¬ 𝑛 < 𝑘 ) → 𝑘 < 𝑛 )
146 145 ad5ant2345 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ 𝑛 = 𝑘 ) ∧ ¬ 𝑛 < 𝑘 ) → 𝑘 < 𝑛 )
147 anass ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ) )
148 incom ⊢ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) ∩ ( 𝐹 ‘ 𝑛 ) )
149 148 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ) ∧ 𝑘 < 𝑛 ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) ∩ ( 𝐹 ‘ 𝑛 ) ) )
150 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ) ∧ 𝑘 < 𝑛 ) → 𝑘 ∈ 𝑍 )
151 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ) ∧ 𝑘 < 𝑛 ) → 𝑛 ∈ 𝑍 )
152 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ) ∧ 𝑘 < 𝑛 ) → 𝑘 < 𝑛 )
153 2 116 150 151 152 iundjiunlem ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ) ∧ 𝑘 < 𝑛 ) → ( ( 𝐹 ‘ 𝑘 ) ∩ ( 𝐹 ‘ 𝑛 ) ) = ∅ )
154 149 153 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ) ∧ 𝑘 < 𝑛 ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ )
155 147 154 sylanb ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑘 < 𝑛 ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ )
156 122 146 155 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ 𝑛 = 𝑘 ) ∧ ¬ 𝑛 < 𝑘 ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ )
157 121 156 pm2.61dan ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ 𝑛 = 𝑘 ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ )
158 157 ex ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) → ( ¬ 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) )
159 df-or ⊢ ( ( 𝑛 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) ↔ ( ¬ 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) )
160 158 159 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑛 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) )
161 160 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∀ 𝑘 ∈ 𝑍 ( 𝑛 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) )
162 161 ex ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 → ∀ 𝑘 ∈ 𝑍 ( 𝑛 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) ) )
163 1 162 ralrimi ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ 𝑍 ( 𝑛 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) )
164 nfcv ⊢ Ⅎ 𝑚 ( 𝐹 ‘ 𝑛 )
165 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
166 4 165 nfcxfr ⊢ Ⅎ 𝑛 𝐹
167 nfcv ⊢ Ⅎ 𝑛 𝑚
168 166 167 nffv ⊢ Ⅎ 𝑛 ( 𝐹 ‘ 𝑚 )
169 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
170 164 168 169 cbvdisj ⊢ ( Disj 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ↔ Disj 𝑚 ∈ 𝑍 ( 𝐹 ‘ 𝑚 ) )
171 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
172 171 disjor ⊢ ( Disj 𝑚 ∈ 𝑍 ( 𝐹 ‘ 𝑚 ) ↔ ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ 𝑍 ( 𝑚 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑚 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) )
173 nfcv ⊢ Ⅎ 𝑛 𝑍
174 nfv ⊢ Ⅎ 𝑛 𝑚 = 𝑘
175 nfcv ⊢ Ⅎ 𝑛 𝑘
176 166 175 nffv ⊢ Ⅎ 𝑛 ( 𝐹 ‘ 𝑘 )
177 168 176 nfin ⊢ Ⅎ 𝑛 ( ( 𝐹 ‘ 𝑚 ) ∩ ( 𝐹 ‘ 𝑘 ) )
178 nfcv ⊢ Ⅎ 𝑛 ∅
179 177 178 nfeq ⊢ Ⅎ 𝑛 ( ( 𝐹 ‘ 𝑚 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅
180 174 179 nfor ⊢ Ⅎ 𝑛 ( 𝑚 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑚 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ )
181 173 180 nfralw ⊢ Ⅎ 𝑛 ∀ 𝑘 ∈ 𝑍 ( 𝑚 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑚 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ )
182 nfv ⊢ Ⅎ 𝑚 ∀ 𝑘 ∈ 𝑍 ( 𝑛 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ )
183 equequ1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 = 𝑘 ↔ 𝑛 = 𝑘 ) )
184 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
185 184 ineq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐹 ‘ 𝑚 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) )
186 185 eqeq1d ⊢ ( 𝑚 = 𝑛 → ( ( ( 𝐹 ‘ 𝑚 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ↔ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) )
187 183 186 orbi12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑚 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) ↔ ( 𝑛 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) ) )
188 187 ralbidv ⊢ ( 𝑚 = 𝑛 → ( ∀ 𝑘 ∈ 𝑍 ( 𝑚 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑚 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) ↔ ∀ 𝑘 ∈ 𝑍 ( 𝑛 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) ) )
189 181 182 188 cbvralw ⊢ ( ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ 𝑍 ( 𝑚 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑚 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) ↔ ∀ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ 𝑍 ( 𝑛 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) )
190 170 172 189 3bitri ⊢ ( Disj 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ 𝑍 ( 𝑛 = 𝑘 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑘 ) ) = ∅ ) )
191 163 190 sylibr ⊢ ( 𝜑 → Disj 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) )
192 108 110 191 jca31 ⊢ ( 𝜑 → ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ∧ ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∧ Disj 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ) )