Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ennnfoneleminc GIF version

Theorem ennnfoneleminc 11980
 Description: Lemma for ennnfone 11994. We only add elements to 𝐻 as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.)
Hypotheses
Ref Expression
ennnfonelemh.dceq (𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
ennnfonelemh.f (𝜑𝐹:ω–onto𝐴)
ennnfonelemh.ne (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
ennnfonelemh.g 𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))
ennnfonelemh.n 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
ennnfonelemh.j 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))
ennnfonelemh.h 𝐻 = seq0(𝐺, 𝐽)
ennnfoneleminc.p (𝜑𝑃 ∈ ℕ0)
ennnfoneleminc.q (𝜑𝑄 ∈ ℕ0)
ennnfoneleminc.le (𝜑𝑃𝑄)
Assertion
Ref Expression
ennnfoneleminc (𝜑 → (𝐻𝑃) ⊆ (𝐻𝑄))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑛,𝐹,𝑗,𝑘   𝑥,𝐹,𝑦   𝑥,𝐻,𝑦   𝑥,𝑁,𝑦   𝑥,𝑃,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑗,𝑘,𝑛)   𝐴(𝑗,𝑘,𝑛)   𝑃(𝑗,𝑘,𝑛)   𝑄(𝑥,𝑦,𝑗,𝑘,𝑛)   𝐺(𝑥,𝑦,𝑗,𝑘,𝑛)   𝐻(𝑗,𝑘,𝑛)   𝐽(𝑥,𝑦,𝑗,𝑘,𝑛)   𝑁(𝑗,𝑘,𝑛)

Proof of Theorem ennnfoneleminc
Dummy variables 𝑐 𝑎 𝑏 𝑟 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ennnfoneleminc.p . . . 4 (𝜑𝑃 ∈ ℕ0)
21nn0zd 9215 . . 3 (𝜑𝑃 ∈ ℤ)
3 ennnfoneleminc.q . . . 4 (𝜑𝑄 ∈ ℕ0)
43nn0zd 9215 . . 3 (𝜑𝑄 ∈ ℤ)
5 ennnfoneleminc.le . . 3 (𝜑𝑃𝑄)
62, 4, 53jca 1162 . 2 (𝜑 → (𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ 𝑃𝑄))
7 fveq2 5430 . . . . 5 (𝑤 = 𝑃 → (𝐻𝑤) = (𝐻𝑃))
87sseq2d 3133 . . . 4 (𝑤 = 𝑃 → ((𝐻𝑃) ⊆ (𝐻𝑤) ↔ (𝐻𝑃) ⊆ (𝐻𝑃)))
98imbi2d 229 . . 3 (𝑤 = 𝑃 → ((𝜑 → (𝐻𝑃) ⊆ (𝐻𝑤)) ↔ (𝜑 → (𝐻𝑃) ⊆ (𝐻𝑃))))
10 fveq2 5430 . . . . 5 (𝑤 = 𝑟 → (𝐻𝑤) = (𝐻𝑟))
1110sseq2d 3133 . . . 4 (𝑤 = 𝑟 → ((𝐻𝑃) ⊆ (𝐻𝑤) ↔ (𝐻𝑃) ⊆ (𝐻𝑟)))
1211imbi2d 229 . . 3 (𝑤 = 𝑟 → ((𝜑 → (𝐻𝑃) ⊆ (𝐻𝑤)) ↔ (𝜑 → (𝐻𝑃) ⊆ (𝐻𝑟))))
13 fveq2 5430 . . . . 5 (𝑤 = (𝑟 + 1) → (𝐻𝑤) = (𝐻‘(𝑟 + 1)))
1413sseq2d 3133 . . . 4 (𝑤 = (𝑟 + 1) → ((𝐻𝑃) ⊆ (𝐻𝑤) ↔ (𝐻𝑃) ⊆ (𝐻‘(𝑟 + 1))))
1514imbi2d 229 . . 3 (𝑤 = (𝑟 + 1) → ((𝜑 → (𝐻𝑃) ⊆ (𝐻𝑤)) ↔ (𝜑 → (𝐻𝑃) ⊆ (𝐻‘(𝑟 + 1)))))
16 fveq2 5430 . . . . 5 (𝑤 = 𝑄 → (𝐻𝑤) = (𝐻𝑄))
1716sseq2d 3133 . . . 4 (𝑤 = 𝑄 → ((𝐻𝑃) ⊆ (𝐻𝑤) ↔ (𝐻𝑃) ⊆ (𝐻𝑄)))
1817imbi2d 229 . . 3 (𝑤 = 𝑄 → ((𝜑 → (𝐻𝑃) ⊆ (𝐻𝑤)) ↔ (𝜑 → (𝐻𝑃) ⊆ (𝐻𝑄))))
19 ssidd 3124 . . . 4 (𝑃 ∈ ℤ → (𝐻𝑃) ⊆ (𝐻𝑃))
2019a1d 22 . . 3 (𝑃 ∈ ℤ → (𝜑 → (𝐻𝑃) ⊆ (𝐻𝑃)))
21 simpr 109 . . . . . . 7 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → (𝐻𝑃) ⊆ (𝐻𝑟))
22 ennnfonelemh.dceq . . . . . . . . 9 (𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
2322ad2antrr 480 . . . . . . . 8 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
24 ennnfonelemh.f . . . . . . . . 9 (𝜑𝐹:ω–onto𝐴)
2524ad2antrr 480 . . . . . . . 8 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → 𝐹:ω–onto𝐴)
26 ennnfonelemh.ne . . . . . . . . . 10 (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
2726ad2antrr 480 . . . . . . . . 9 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
28 fveq2 5430 . . . . . . . . . . . . . . 15 (𝑗 = 𝑐 → (𝐹𝑗) = (𝐹𝑐))
2928neeq2d 2328 . . . . . . . . . . . . . 14 (𝑗 = 𝑐 → ((𝐹𝑘) ≠ (𝐹𝑗) ↔ (𝐹𝑘) ≠ (𝐹𝑐)))
3029cbvralv 2658 . . . . . . . . . . . . 13 (∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∀𝑐 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑐))
3130rexbii 2446 . . . . . . . . . . . 12 (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∃𝑘 ∈ ω ∀𝑐 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑐))
32 fveq2 5430 . . . . . . . . . . . . . . 15 (𝑘 = 𝑏 → (𝐹𝑘) = (𝐹𝑏))
3332neeq1d 2327 . . . . . . . . . . . . . 14 (𝑘 = 𝑏 → ((𝐹𝑘) ≠ (𝐹𝑐) ↔ (𝐹𝑏) ≠ (𝐹𝑐)))
3433ralbidv 2439 . . . . . . . . . . . . 13 (𝑘 = 𝑏 → (∀𝑐 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑐) ↔ ∀𝑐 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑐)))
3534cbvrexv 2659 . . . . . . . . . . . 12 (∃𝑘 ∈ ω ∀𝑐 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑐) ↔ ∃𝑏 ∈ ω ∀𝑐 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑐))
3631, 35bitri 183 . . . . . . . . . . 11 (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∃𝑏 ∈ ω ∀𝑐 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑐))
3736ralbii 2445 . . . . . . . . . 10 (∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∀𝑛 ∈ ω ∃𝑏 ∈ ω ∀𝑐 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑐))
38 suceq 4333 . . . . . . . . . . . . 13 (𝑛 = 𝑎 → suc 𝑛 = suc 𝑎)
3938raleqdv 2636 . . . . . . . . . . . 12 (𝑛 = 𝑎 → (∀𝑐 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑐) ↔ ∀𝑐 ∈ suc 𝑎(𝐹𝑏) ≠ (𝐹𝑐)))
4039rexbidv 2440 . . . . . . . . . . 11 (𝑛 = 𝑎 → (∃𝑏 ∈ ω ∀𝑐 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑐) ↔ ∃𝑏 ∈ ω ∀𝑐 ∈ suc 𝑎(𝐹𝑏) ≠ (𝐹𝑐)))
4140cbvralv 2658 . . . . . . . . . 10 (∀𝑛 ∈ ω ∃𝑏 ∈ ω ∀𝑐 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑐) ↔ ∀𝑎 ∈ ω ∃𝑏 ∈ ω ∀𝑐 ∈ suc 𝑎(𝐹𝑏) ≠ (𝐹𝑐))
4237, 41bitri 183 . . . . . . . . 9 (∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∀𝑎 ∈ ω ∃𝑏 ∈ ω ∀𝑐 ∈ suc 𝑎(𝐹𝑏) ≠ (𝐹𝑐))
4327, 42sylib 121 . . . . . . . 8 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → ∀𝑎 ∈ ω ∃𝑏 ∈ ω ∀𝑐 ∈ suc 𝑎(𝐹𝑏) ≠ (𝐹𝑐))
44 ennnfonelemh.g . . . . . . . 8 𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))
45 ennnfonelemh.n . . . . . . . 8 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
46 ennnfonelemh.j . . . . . . . 8 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))
47 ennnfonelemh.h . . . . . . . 8 𝐻 = seq0(𝐺, 𝐽)
48 simplr2 1025 . . . . . . . . 9 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → 𝑟 ∈ ℤ)
49 0red 7811 . . . . . . . . . 10 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → 0 ∈ ℝ)
501nn0red 9075 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℝ)
5150ad2antrr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → 𝑃 ∈ ℝ)
5248zred 9217 . . . . . . . . . 10 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → 𝑟 ∈ ℝ)
531nn0ge0d 9077 . . . . . . . . . . 11 (𝜑 → 0 ≤ 𝑃)
5453ad2antrr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → 0 ≤ 𝑃)
55 simplr3 1026 . . . . . . . . . 10 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → 𝑃𝑟)
5649, 51, 52, 54, 55letrd 7930 . . . . . . . . 9 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → 0 ≤ 𝑟)
57 elnn0z 9111 . . . . . . . . 9 (𝑟 ∈ ℕ0 ↔ (𝑟 ∈ ℤ ∧ 0 ≤ 𝑟))
5848, 56, 57sylanbrc 414 . . . . . . . 8 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → 𝑟 ∈ ℕ0)
5923, 25, 43, 44, 45, 46, 47, 58ennnfonelemss 11979 . . . . . . 7 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → (𝐻𝑟) ⊆ (𝐻‘(𝑟 + 1)))
6021, 59sstrd 3113 . . . . . 6 (((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) ∧ (𝐻𝑃) ⊆ (𝐻𝑟)) → (𝐻𝑃) ⊆ (𝐻‘(𝑟 + 1)))
6160ex 114 . . . . 5 ((𝜑 ∧ (𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟)) → ((𝐻𝑃) ⊆ (𝐻𝑟) → (𝐻𝑃) ⊆ (𝐻‘(𝑟 + 1))))
6261expcom 115 . . . 4 ((𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟) → (𝜑 → ((𝐻𝑃) ⊆ (𝐻𝑟) → (𝐻𝑃) ⊆ (𝐻‘(𝑟 + 1)))))
6362a2d 26 . . 3 ((𝑃 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝑃𝑟) → ((𝜑 → (𝐻𝑃) ⊆ (𝐻𝑟)) → (𝜑 → (𝐻𝑃) ⊆ (𝐻‘(𝑟 + 1)))))
649, 12, 15, 18, 20, 63uzind 9206 . 2 ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ 𝑃𝑄) → (𝜑 → (𝐻𝑃) ⊆ (𝐻𝑄)))
656, 64mpcom 36 1 (𝜑 → (𝐻𝑃) ⊆ (𝐻𝑄))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103  DECID wdc 820   ∧ w3a 963   = wceq 1332   ∈ wcel 1481   ≠ wne 2309  ∀wral 2417  ∃wrex 2418   ∪ cun 3075   ⊆ wss 3077  ∅c0 3369  ifcif 3480  {csn 3533  ⟨cop 3536   class class class wbr 3938   ↦ cmpt 3998  suc csuc 4296  ωcom 4513  ◡ccnv 4547  dom cdm 4548   “ cima 4551  –onto→wfo 5130  ‘cfv 5132  (class class class)co 5783   ∈ cmpo 5785  freccfrec 6296   ↑pm cpm 6552  ℝcr 7663  0cc0 7664  1c1 7665   + caddc 7667   ≤ cle 7845   − cmin 7977  ℕ0cn0 9021  ℤcz 9098  seqcseq 10269 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-setind 4461  ax-iinf 4511  ax-cnex 7755  ax-resscn 7756  ax-1cn 7757  ax-1re 7758  ax-icn 7759  ax-addcl 7760  ax-addrcl 7761  ax-mulcl 7762  ax-addcom 7764  ax-addass 7766  ax-distr 7768  ax-i2m1 7769  ax-0lt1 7770  ax-0id 7772  ax-rnegex 7773  ax-cnre 7775  ax-pre-ltirr 7776  ax-pre-ltwlin 7777  ax-pre-lttrn 7778  ax-pre-ltadd 7780 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-if 3481  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-tr 4036  df-id 4224  df-iord 4297  df-on 4299  df-ilim 4300  df-suc 4302  df-iom 4514  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-f1 5137  df-fo 5138  df-f1o 5139  df-fv 5140  df-riota 5739  df-ov 5786  df-oprab 5787  df-mpo 5788  df-1st 6047  df-2nd 6048  df-recs 6211  df-frec 6297  df-pm 6554  df-pnf 7846  df-mnf 7847  df-xr 7848  df-ltxr 7849  df-le 7850  df-sub 7979  df-neg 7980  df-inn 8765  df-n0 9022  df-z 9099  df-uz 9371  df-seqfrec 10270 This theorem is referenced by:  ennnfonelemex  11983  ennnfonelemrnh  11985
 Copyright terms: Public domain W3C validator