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

Theorem finxpsuclem 32858
Description: Lemma for finxpsuc 32859. (Contributed by ML, 24-Oct-2020.)
Hypothesis
Ref Expression
finxpsuclem.1 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)))
Assertion
Ref Expression
finxpsuclem ((𝑁 ∈ ω ∧ 1𝑜𝑁) → (𝑈↑↑suc 𝑁) = ((𝑈↑↑𝑁) × 𝑈))
Distinct variable groups:   𝑛,𝑁,𝑥   𝑈,𝑛,𝑥
Allowed substitution hints:   𝐹(𝑥,𝑛)

Proof of Theorem finxpsuclem
Dummy variables 𝑧 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano2 7034 . . . . . . . . . 10 (𝑁 ∈ ω → suc 𝑁 ∈ ω)
21adantr 481 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → suc 𝑁 ∈ ω)
3 1on 7513 . . . . . . . . . . . . 13 1𝑜 ∈ On
43onordi 5794 . . . . . . . . . . . 12 Ord 1𝑜
5 nnord 7021 . . . . . . . . . . . 12 (𝑁 ∈ ω → Ord 𝑁)
6 ordsseleq 5714 . . . . . . . . . . . 12 ((Ord 1𝑜 ∧ Ord 𝑁) → (1𝑜𝑁 ↔ (1𝑜𝑁 ∨ 1𝑜 = 𝑁)))
74, 5, 6sylancr 694 . . . . . . . . . . 11 (𝑁 ∈ ω → (1𝑜𝑁 ↔ (1𝑜𝑁 ∨ 1𝑜 = 𝑁)))
87biimpa 501 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → (1𝑜𝑁 ∨ 1𝑜 = 𝑁))
9 elelsuc 5759 . . . . . . . . . . . . 13 (1𝑜𝑁 → 1𝑜 ∈ suc 𝑁)
109a1i 11 . . . . . . . . . . . 12 (𝑁 ∈ ω → (1𝑜𝑁 → 1𝑜 ∈ suc 𝑁))
11 sucidg 5765 . . . . . . . . . . . . 13 (𝑁 ∈ ω → 𝑁 ∈ suc 𝑁)
12 eleq1 2692 . . . . . . . . . . . . 13 (1𝑜 = 𝑁 → (1𝑜 ∈ suc 𝑁𝑁 ∈ suc 𝑁))
1311, 12syl5ibrcom 237 . . . . . . . . . . . 12 (𝑁 ∈ ω → (1𝑜 = 𝑁 → 1𝑜 ∈ suc 𝑁))
1410, 13jaod 395 . . . . . . . . . . 11 (𝑁 ∈ ω → ((1𝑜𝑁 ∨ 1𝑜 = 𝑁) → 1𝑜 ∈ suc 𝑁))
1514adantr 481 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → ((1𝑜𝑁 ∨ 1𝑜 = 𝑁) → 1𝑜 ∈ suc 𝑁))
168, 15mpd 15 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → 1𝑜 ∈ suc 𝑁)
17 finxpsuclem.1 . . . . . . . . . 10 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)))
1817finxpreclem6 32857 . . . . . . . . 9 ((suc 𝑁 ∈ ω ∧ 1𝑜 ∈ suc 𝑁) → (𝑈↑↑suc 𝑁) ⊆ (V × 𝑈))
192, 16, 18syl2anc 692 . . . . . . . 8 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → (𝑈↑↑suc 𝑁) ⊆ (V × 𝑈))
2019sselda 3588 . . . . . . 7 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (𝑈↑↑suc 𝑁)) → 𝑦 ∈ (V × 𝑈))
211ad2antrr 761 . . . . . . . . . . . . 13 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → suc 𝑁 ∈ ω)
22 df-2o 7507 . . . . . . . . . . . . . . 15 2𝑜 = suc 1𝑜
23 ordsucsssuc 6971 . . . . . . . . . . . . . . . . 17 ((Ord 1𝑜 ∧ Ord 𝑁) → (1𝑜𝑁 ↔ suc 1𝑜 ⊆ suc 𝑁))
244, 5, 23sylancr 694 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ω → (1𝑜𝑁 ↔ suc 1𝑜 ⊆ suc 𝑁))
2524biimpa 501 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → suc 1𝑜 ⊆ suc 𝑁)
2622, 25syl5eqss 3633 . . . . . . . . . . . . . 14 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → 2𝑜 ⊆ suc 𝑁)
2726adantr 481 . . . . . . . . . . . . 13 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → 2𝑜 ⊆ suc 𝑁)
28 simpr 477 . . . . . . . . . . . . 13 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → 𝑦 ∈ (V × 𝑈))
2917finxpreclem4 32855 . . . . . . . . . . . . 13 (((suc 𝑁 ∈ ω ∧ 2𝑜 ⊆ suc 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁) = (rec(𝐹, ⟨ suc 𝑁, (1st𝑦)⟩)‘ suc 𝑁))
3021, 27, 28, 29syl21anc 1322 . . . . . . . . . . . 12 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁) = (rec(𝐹, ⟨ suc 𝑁, (1st𝑦)⟩)‘ suc 𝑁))
31 ordunisuc 6980 . . . . . . . . . . . . . . . 16 (Ord 𝑁 suc 𝑁 = 𝑁)
325, 31syl 17 . . . . . . . . . . . . . . 15 (𝑁 ∈ ω → suc 𝑁 = 𝑁)
33 opeq1 4375 . . . . . . . . . . . . . . . 16 ( suc 𝑁 = 𝑁 → ⟨ suc 𝑁, (1st𝑦)⟩ = ⟨𝑁, (1st𝑦)⟩)
34 rdgeq2 7454 . . . . . . . . . . . . . . . 16 (⟨ suc 𝑁, (1st𝑦)⟩ = ⟨𝑁, (1st𝑦)⟩ → rec(𝐹, ⟨ suc 𝑁, (1st𝑦)⟩) = rec(𝐹, ⟨𝑁, (1st𝑦)⟩))
3533, 34syl 17 . . . . . . . . . . . . . . 15 ( suc 𝑁 = 𝑁 → rec(𝐹, ⟨ suc 𝑁, (1st𝑦)⟩) = rec(𝐹, ⟨𝑁, (1st𝑦)⟩))
3632, 35syl 17 . . . . . . . . . . . . . 14 (𝑁 ∈ ω → rec(𝐹, ⟨ suc 𝑁, (1st𝑦)⟩) = rec(𝐹, ⟨𝑁, (1st𝑦)⟩))
3736, 32fveq12d 6156 . . . . . . . . . . . . 13 (𝑁 ∈ ω → (rec(𝐹, ⟨ suc 𝑁, (1st𝑦)⟩)‘ suc 𝑁) = (rec(𝐹, ⟨𝑁, (1st𝑦)⟩)‘𝑁))
3837ad2antrr 761 . . . . . . . . . . . 12 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨ suc 𝑁, (1st𝑦)⟩)‘ suc 𝑁) = (rec(𝐹, ⟨𝑁, (1st𝑦)⟩)‘𝑁))
3930, 38eqtrd 2660 . . . . . . . . . . 11 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁) = (rec(𝐹, ⟨𝑁, (1st𝑦)⟩)‘𝑁))
4039eqeq2d 2636 . . . . . . . . . 10 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁) ↔ ∅ = (rec(𝐹, ⟨𝑁, (1st𝑦)⟩)‘𝑁)))
411biantrurd 529 . . . . . . . . . . . 12 (𝑁 ∈ ω → (∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁) ↔ (suc 𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁))))
4217dffinxpf 32846 . . . . . . . . . . . . 13 (𝑈↑↑suc 𝑁) = {𝑦 ∣ (suc 𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁))}
4342abeq2i 2738 . . . . . . . . . . . 12 (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ (suc 𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁)))
4441, 43syl6rbbr 279 . . . . . . . . . . 11 (𝑁 ∈ ω → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ ∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁)))
4544ad2antrr 761 . . . . . . . . . 10 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ ∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁)))
46 fvex 6160 . . . . . . . . . . . . 13 (1st𝑦) ∈ V
47 opeq2 4376 . . . . . . . . . . . . . . . . 17 (𝑧 = (1st𝑦) → ⟨𝑁, 𝑧⟩ = ⟨𝑁, (1st𝑦)⟩)
48 rdgeq2 7454 . . . . . . . . . . . . . . . . 17 (⟨𝑁, 𝑧⟩ = ⟨𝑁, (1st𝑦)⟩ → rec(𝐹, ⟨𝑁, 𝑧⟩) = rec(𝐹, ⟨𝑁, (1st𝑦)⟩))
4947, 48syl 17 . . . . . . . . . . . . . . . 16 (𝑧 = (1st𝑦) → rec(𝐹, ⟨𝑁, 𝑧⟩) = rec(𝐹, ⟨𝑁, (1st𝑦)⟩))
5049fveq1d 6152 . . . . . . . . . . . . . . 15 (𝑧 = (1st𝑦) → (rec(𝐹, ⟨𝑁, 𝑧⟩)‘𝑁) = (rec(𝐹, ⟨𝑁, (1st𝑦)⟩)‘𝑁))
5150eqeq2d 2636 . . . . . . . . . . . . . 14 (𝑧 = (1st𝑦) → (∅ = (rec(𝐹, ⟨𝑁, 𝑧⟩)‘𝑁) ↔ ∅ = (rec(𝐹, ⟨𝑁, (1st𝑦)⟩)‘𝑁)))
5251anbi2d 739 . . . . . . . . . . . . 13 (𝑧 = (1st𝑦) → ((𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, 𝑧⟩)‘𝑁)) ↔ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, (1st𝑦)⟩)‘𝑁))))
5317dffinxpf 32846 . . . . . . . . . . . . 13 (𝑈↑↑𝑁) = {𝑧 ∣ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, 𝑧⟩)‘𝑁))}
5446, 52, 53elab2 3342 . . . . . . . . . . . 12 ((1st𝑦) ∈ (𝑈↑↑𝑁) ↔ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, (1st𝑦)⟩)‘𝑁)))
5554baib 943 . . . . . . . . . . 11 (𝑁 ∈ ω → ((1st𝑦) ∈ (𝑈↑↑𝑁) ↔ ∅ = (rec(𝐹, ⟨𝑁, (1st𝑦)⟩)‘𝑁)))
5655ad2antrr 761 . . . . . . . . . 10 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → ((1st𝑦) ∈ (𝑈↑↑𝑁) ↔ ∅ = (rec(𝐹, ⟨𝑁, (1st𝑦)⟩)‘𝑁)))
5740, 45, 563bitr4d 300 . . . . . . . . 9 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ (1st𝑦) ∈ (𝑈↑↑𝑁)))
5857biimpd 219 . . . . . . . 8 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝑦 ∈ (𝑈↑↑suc 𝑁) → (1st𝑦) ∈ (𝑈↑↑𝑁)))
5958impancom 456 . . . . . . 7 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (𝑈↑↑suc 𝑁)) → (𝑦 ∈ (V × 𝑈) → (1st𝑦) ∈ (𝑈↑↑𝑁)))
6020, 59mpd 15 . . . . . 6 (((𝑁 ∈ ω ∧ 1𝑜𝑁) ∧ 𝑦 ∈ (𝑈↑↑suc 𝑁)) → (1st𝑦) ∈ (𝑈↑↑𝑁))
6160ex 450 . . . . 5 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → (𝑦 ∈ (𝑈↑↑suc 𝑁) → (1st𝑦) ∈ (𝑈↑↑𝑁)))
6220ex 450 . . . . 5 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → (𝑦 ∈ (𝑈↑↑suc 𝑁) → 𝑦 ∈ (V × 𝑈)))
6361, 62jcad 555 . . . 4 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → (𝑦 ∈ (𝑈↑↑suc 𝑁) → ((1st𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈))))
6457exbiri 651 . . . . . 6 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → (𝑦 ∈ (V × 𝑈) → ((1st𝑦) ∈ (𝑈↑↑𝑁) → 𝑦 ∈ (𝑈↑↑suc 𝑁))))
6564impd 447 . . . . 5 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → ((𝑦 ∈ (V × 𝑈) ∧ (1st𝑦) ∈ (𝑈↑↑𝑁)) → 𝑦 ∈ (𝑈↑↑suc 𝑁)))
6665ancomsd 470 . . . 4 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → (((1st𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → 𝑦 ∈ (𝑈↑↑suc 𝑁)))
6763, 66impbid 202 . . 3 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ ((1st𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈))))
68 elxp8 32843 . . 3 (𝑦 ∈ ((𝑈↑↑𝑁) × 𝑈) ↔ ((1st𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈)))
6967, 68syl6bbr 278 . 2 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ 𝑦 ∈ ((𝑈↑↑𝑁) × 𝑈)))
7069eqrdv 2624 1 ((𝑁 ∈ ω ∧ 1𝑜𝑁) → (𝑈↑↑suc 𝑁) = ((𝑈↑↑𝑁) × 𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1992  Vcvv 3191  wss 3560  c0 3896  ifcif 4063  cop 4159   cuni 4407   × cxp 5077  Ord word 5684  suc csuc 5687  cfv 5850  cmpt2 6607  ωcom 7013  1st c1st 7114  reccrdg 7451  1𝑜c1o 7499  2𝑜c2o 7500  ↑↑cfinxp 32844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-reg 8442
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-2o 7507  df-oadd 7510  df-er 7688  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-finxp 32845
This theorem is referenced by:  finxpsuc  32859
  Copyright terms: Public domain W3C validator