Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  trpredlem1 Structured version   Visualization version   GIF version

Theorem trpredlem1 32045
Description: Technical lemma for transitive predecessors properties. All values of the transitive predecessors' underlying function are subsets of the base set. (Contributed by Scott Fenton, 28-Apr-2012.)
Assertion
Ref Expression
trpredlem1 (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴)
Distinct variable groups:   𝐴,𝑎,𝑦   𝑅,𝑎,𝑦   𝑋,𝑎
Allowed substitution hints:   𝐴(𝑖)   𝐵(𝑦,𝑖,𝑎)   𝑅(𝑖)   𝑋(𝑦,𝑖)

Proof of Theorem trpredlem1
Dummy variables 𝑒 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0suc 7316 . . 3 (𝑖 ∈ ω → (𝑖 = ∅ ∨ ∃𝑗 ∈ ω 𝑖 = suc 𝑗))
2 fr0g 7763 . . . . . 6 (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
3 predss 5900 . . . . . 6 Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴
42, 3syl6eqss 3852 . . . . 5 (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ⊆ 𝐴)
5 fveq2 6404 . . . . . 6 (𝑖 = ∅ → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) = ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅))
65sseq1d 3829 . . . . 5 (𝑖 = ∅ → (((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴 ↔ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ⊆ 𝐴))
74, 6syl5ibr 237 . . . 4 (𝑖 = ∅ → (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴))
8 nfcv 2948 . . . . . . . . . . 11 𝑎Pred(𝑅, 𝐴, 𝑋)
9 nfcv 2948 . . . . . . . . . . 11 𝑎𝑗
10 nfmpt1 4941 . . . . . . . . . . . . . . 15 𝑎(𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦))
1110, 8nfrdg 7742 . . . . . . . . . . . . . 14 𝑎rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋))
12 nfcv 2948 . . . . . . . . . . . . . 14 𝑎ω
1311, 12nfres 5599 . . . . . . . . . . . . 13 𝑎(rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)
1413, 9nffv 6414 . . . . . . . . . . . 12 𝑎((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)
15 nfcv 2948 . . . . . . . . . . . 12 𝑎Pred(𝑅, 𝐴, 𝑒)
1614, 15nfiun 4740 . . . . . . . . . . 11 𝑎 𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑒)
17 predeq3 5897 . . . . . . . . . . . . . 14 (𝑦 = 𝑒 → Pred(𝑅, 𝐴, 𝑦) = Pred(𝑅, 𝐴, 𝑒))
1817cbviunv 4751 . . . . . . . . . . . . 13 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦) = 𝑒𝑎 Pred(𝑅, 𝐴, 𝑒)
1918mpteq2i 4935 . . . . . . . . . . . 12 (𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)) = (𝑎 ∈ V ↦ 𝑒𝑎 Pred(𝑅, 𝐴, 𝑒))
20 rdgeq1 7739 . . . . . . . . . . . 12 ((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)) = (𝑎 ∈ V ↦ 𝑒𝑎 Pred(𝑅, 𝐴, 𝑒)) → rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) = rec((𝑎 ∈ V ↦ 𝑒𝑎 Pred(𝑅, 𝐴, 𝑒)), Pred(𝑅, 𝐴, 𝑋)))
21 reseq1 5591 . . . . . . . . . . . 12 (rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) = rec((𝑎 ∈ V ↦ 𝑒𝑎 Pred(𝑅, 𝐴, 𝑒)), Pred(𝑅, 𝐴, 𝑋)) → (rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) = (rec((𝑎 ∈ V ↦ 𝑒𝑎 Pred(𝑅, 𝐴, 𝑒)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω))
2219, 20, 21mp2b 10 . . . . . . . . . . 11 (rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) = (rec((𝑎 ∈ V ↦ 𝑒𝑎 Pred(𝑅, 𝐴, 𝑒)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)
23 iuneq1 4726 . . . . . . . . . . 11 (𝑎 = ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → 𝑒𝑎 Pred(𝑅, 𝐴, 𝑒) = 𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑒))
248, 9, 16, 22, 23frsucmpt 7765 . . . . . . . . . 10 ((𝑗 ∈ ω ∧ 𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑒) ∈ V) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) = 𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑒))
25 iunss 4753 . . . . . . . . . . 11 ( 𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑒) ⊆ 𝐴 ↔ ∀𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑒) ⊆ 𝐴)
26 predss 5900 . . . . . . . . . . . 12 Pred(𝑅, 𝐴, 𝑒) ⊆ 𝐴
2726a1i 11 . . . . . . . . . . 11 (𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → Pred(𝑅, 𝐴, 𝑒) ⊆ 𝐴)
2825, 27mprgbir 3115 . . . . . . . . . 10 𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑒) ⊆ 𝐴
2924, 28syl6eqss 3852 . . . . . . . . 9 ((𝑗 ∈ ω ∧ 𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑒) ∈ V) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) ⊆ 𝐴)
308, 9, 16, 22, 23frsucmptn 7766 . . . . . . . . . . 11 𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑒) ∈ V → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) = ∅)
3130adantl 469 . . . . . . . . . 10 ((𝑗 ∈ ω ∧ ¬ 𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑒) ∈ V) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) = ∅)
32 0ss 4170 . . . . . . . . . 10 ∅ ⊆ 𝐴
3331, 32syl6eqss 3852 . . . . . . . . 9 ((𝑗 ∈ ω ∧ ¬ 𝑒 ∈ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑒) ∈ V) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) ⊆ 𝐴)
3429, 33pm2.61dan 838 . . . . . . . 8 (𝑗 ∈ ω → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) ⊆ 𝐴)
3534adantr 468 . . . . . . 7 ((𝑗 ∈ ω ∧ 𝑖 = suc 𝑗) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) ⊆ 𝐴)
36 fveq2 6404 . . . . . . . . 9 (𝑖 = suc 𝑗 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) = ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗))
3736sseq1d 3829 . . . . . . . 8 (𝑖 = suc 𝑗 → (((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴 ↔ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) ⊆ 𝐴))
3837adantl 469 . . . . . . 7 ((𝑗 ∈ ω ∧ 𝑖 = suc 𝑗) → (((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴 ↔ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) ⊆ 𝐴))
3935, 38mpbird 248 . . . . . 6 ((𝑗 ∈ ω ∧ 𝑖 = suc 𝑗) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴)
4039rexlimiva 3216 . . . . 5 (∃𝑗 ∈ ω 𝑖 = suc 𝑗 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴)
4140a1d 25 . . . 4 (∃𝑗 ∈ ω 𝑖 = suc 𝑗 → (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴))
427, 41jaoi 875 . . 3 ((𝑖 = ∅ ∨ ∃𝑗 ∈ ω 𝑖 = suc 𝑗) → (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴))
431, 42syl 17 . 2 (𝑖 ∈ ω → (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴))
44 nfvres 6440 . . . 4 𝑖 ∈ ω → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) = ∅)
4544, 32syl6eqss 3852 . . 3 𝑖 ∈ ω → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴)
4645a1d 25 . 2 𝑖 ∈ ω → (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴))
4743, 46pm2.61i 176 1 (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wcel 2156  wrex 3097  Vcvv 3391  wss 3769  c0 4116   ciun 4712  cmpt 4923  cres 5313  Predcpred 5892  suc csuc 5938  cfv 6097  ωcom 7291  reccrdg 7737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-om 7292  df-wrecs 7638  df-recs 7700  df-rdg 7738
This theorem is referenced by:  trpredss  32047  trpredtr  32048  trpredmintr  32049  trpredrec  32056
  Copyright terms: Public domain W3C validator