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

Theorem mnurndlem1 43122
Description: Lemma for mnurnd 43124. (Contributed by Rohan Ridenour, 12-Aug-2023.)
Hypotheses
Ref Expression
mnurndlem1.3 (𝜑𝐹:𝐴𝑈)
mnurndlem1.4 𝐴 ∈ V
mnurndlem1.6 (𝜑 → ∀𝑖𝐴 (∃𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣 → ∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤)))
Assertion
Ref Expression
mnurndlem1 (𝜑 → ran 𝐹𝑤)
Distinct variable groups:   𝑣,𝐹   𝑤,𝑢,𝑖,𝑎   𝑣,𝐴,𝑖,𝑎   𝑢,𝐴   𝑢,𝐹,𝑖,𝑎
Allowed substitution hints:   𝜑(𝑤,𝑣,𝑢,𝑖,𝑎)   𝐴(𝑤)   𝑈(𝑤,𝑣,𝑢,𝑖,𝑎)   𝐹(𝑤)

Proof of Theorem mnurndlem1
StepHypRef Expression
1 mnurndlem1.3 . . 3 (𝜑𝐹:𝐴𝑈)
21ffnd 6718 . 2 (𝜑𝐹 Fn 𝐴)
3 mnurndlem1.6 . . . 4 (𝜑 → ∀𝑖𝐴 (∃𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣 → ∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤)))
4 vex 3478 . . . . . . . 8 𝑖 ∈ V
54prid1 4766 . . . . . . 7 𝑖 ∈ {𝑖, {(𝐹𝑖), 𝐴}}
6 simpr 485 . . . . . . 7 ((𝑖𝐴𝑣 = {𝑖, {(𝐹𝑖), 𝐴}}) → 𝑣 = {𝑖, {(𝐹𝑖), 𝐴}})
75, 6eleqtrrid 2840 . . . . . 6 ((𝑖𝐴𝑣 = {𝑖, {(𝐹𝑖), 𝐴}}) → 𝑖𝑣)
8 eqid 2732 . . . . . . 7 (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}}) = (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})
9 id 22 . . . . . . 7 (𝑖𝐴𝑖𝐴)
10 prex 5432 . . . . . . . 8 {𝑖, {(𝐹𝑖), 𝐴}} ∈ V
1110a1i 11 . . . . . . 7 (𝑖𝐴 → {𝑖, {(𝐹𝑖), 𝐴}} ∈ V)
12 id 22 . . . . . . . . 9 (𝑎 = 𝑖𝑎 = 𝑖)
13 fveq2 6891 . . . . . . . . . 10 (𝑎 = 𝑖 → (𝐹𝑎) = (𝐹𝑖))
1413preq1d 4743 . . . . . . . . 9 (𝑎 = 𝑖 → {(𝐹𝑎), 𝐴} = {(𝐹𝑖), 𝐴})
1512, 14preq12d 4745 . . . . . . . 8 (𝑎 = 𝑖 → {𝑎, {(𝐹𝑎), 𝐴}} = {𝑖, {(𝐹𝑖), 𝐴}})
1615adantl 482 . . . . . . 7 ((𝑖𝐴𝑎 = 𝑖) → {𝑎, {(𝐹𝑎), 𝐴}} = {𝑖, {(𝐹𝑖), 𝐴}})
178, 9, 11, 16rr-elrnmpt3d 43042 . . . . . 6 (𝑖𝐴 → {𝑖, {(𝐹𝑖), 𝐴}} ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}}))
187, 17rspcime 3616 . . . . 5 (𝑖𝐴 → ∃𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣)
1918rgen 3063 . . . 4 𝑖𝐴𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣
20 ralim 3086 . . . 4 (∀𝑖𝐴 (∃𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣 → ∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤)) → (∀𝑖𝐴𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣 → ∀𝑖𝐴𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤)))
213, 19, 20mpisyl 21 . . 3 (𝜑 → ∀𝑖𝐴𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤))
22 prex 5432 . . . . . . . 8 {𝑎, {(𝐹𝑎), 𝐴}} ∈ V
2322rgenw 3065 . . . . . . 7 𝑎𝐴 {𝑎, {(𝐹𝑎), 𝐴}} ∈ V
24 eleq2 2822 . . . . . . . . 9 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → (𝑖𝑢𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}}))
25 unieq 4919 . . . . . . . . . 10 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → 𝑢 = {𝑎, {(𝐹𝑎), 𝐴}})
2625sseq1d 4013 . . . . . . . . 9 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → ( 𝑢𝑤 {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤))
2724, 26anbi12d 631 . . . . . . . 8 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → ((𝑖𝑢 𝑢𝑤) ↔ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)))
288, 27rexrnmptw 7096 . . . . . . 7 (∀𝑎𝐴 {𝑎, {(𝐹𝑎), 𝐴}} ∈ V → (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) ↔ ∃𝑎𝐴 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)))
2923, 28ax-mp 5 . . . . . 6 (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) ↔ ∃𝑎𝐴 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤))
30 simplrl 775 . . . . . . . . . . 11 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → 𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}})
31 simpr 485 . . . . . . . . . . . 12 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → 𝑖𝐴)
32 mnurndlem1.4 . . . . . . . . . . . . . . 15 𝐴 ∈ V
3332prid2 4767 . . . . . . . . . . . . . 14 𝐴 ∈ {(𝐹𝑎), 𝐴}
34 elnotel 9607 . . . . . . . . . . . . . 14 (𝐴 ∈ {(𝐹𝑎), 𝐴} → ¬ {(𝐹𝑎), 𝐴} ∈ 𝐴)
3533, 34ax-mp 5 . . . . . . . . . . . . 13 ¬ {(𝐹𝑎), 𝐴} ∈ 𝐴
3635a1i 11 . . . . . . . . . . . 12 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → ¬ {(𝐹𝑎), 𝐴} ∈ 𝐴)
3731, 36elnelneq2d 43037 . . . . . . . . . . 11 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → ¬ 𝑖 = {(𝐹𝑎), 𝐴})
38 elpri 4650 . . . . . . . . . . . . 13 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} → (𝑖 = 𝑎𝑖 = {(𝐹𝑎), 𝐴}))
3938orcomd 869 . . . . . . . . . . . 12 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} → (𝑖 = {(𝐹𝑎), 𝐴} ∨ 𝑖 = 𝑎))
4039ord 862 . . . . . . . . . . 11 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} → (¬ 𝑖 = {(𝐹𝑎), 𝐴} → 𝑖 = 𝑎))
4130, 37, 40sylc 65 . . . . . . . . . 10 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → 𝑖 = 𝑎)
4241fveq2d 6895 . . . . . . . . 9 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → (𝐹𝑖) = (𝐹𝑎))
43 simplrr 776 . . . . . . . . . 10 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)
44 vex 3478 . . . . . . . . . . . . 13 𝑎 ∈ V
45 prex 5432 . . . . . . . . . . . . 13 {(𝐹𝑎), 𝐴} ∈ V
4644, 45unipr 4926 . . . . . . . . . . . 12 {𝑎, {(𝐹𝑎), 𝐴}} = (𝑎 ∪ {(𝐹𝑎), 𝐴})
4746sseq1i 4010 . . . . . . . . . . 11 ( {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤 ↔ (𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤)
48 unss 4184 . . . . . . . . . . . . 13 ((𝑎𝑤 ∧ {(𝐹𝑎), 𝐴} ⊆ 𝑤) ↔ (𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤)
4948bicomi 223 . . . . . . . . . . . 12 ((𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤 ↔ (𝑎𝑤 ∧ {(𝐹𝑎), 𝐴} ⊆ 𝑤))
5049simprbi 497 . . . . . . . . . . 11 ((𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤 → {(𝐹𝑎), 𝐴} ⊆ 𝑤)
5147, 50sylbi 216 . . . . . . . . . 10 ( {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤 → {(𝐹𝑎), 𝐴} ⊆ 𝑤)
52 fvex 6904 . . . . . . . . . . . . 13 (𝐹𝑎) ∈ V
5352, 32prss 4823 . . . . . . . . . . . 12 (((𝐹𝑎) ∈ 𝑤𝐴𝑤) ↔ {(𝐹𝑎), 𝐴} ⊆ 𝑤)
5453bicomi 223 . . . . . . . . . . 11 ({(𝐹𝑎), 𝐴} ⊆ 𝑤 ↔ ((𝐹𝑎) ∈ 𝑤𝐴𝑤))
5554simplbi 498 . . . . . . . . . 10 ({(𝐹𝑎), 𝐴} ⊆ 𝑤 → (𝐹𝑎) ∈ 𝑤)
5643, 51, 553syl 18 . . . . . . . . 9 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → (𝐹𝑎) ∈ 𝑤)
5742, 56eqeltrd 2833 . . . . . . . 8 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → (𝐹𝑖) ∈ 𝑤)
5857ex 413 . . . . . . 7 ((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) → (𝑖𝐴 → (𝐹𝑖) ∈ 𝑤))
5958rexlimiva 3147 . . . . . 6 (∃𝑎𝐴 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤) → (𝑖𝐴 → (𝐹𝑖) ∈ 𝑤))
6029, 59sylbi 216 . . . . 5 (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) → (𝑖𝐴 → (𝐹𝑖) ∈ 𝑤))
6160com12 32 . . . 4 (𝑖𝐴 → (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) → (𝐹𝑖) ∈ 𝑤))
6261ralimia 3080 . . 3 (∀𝑖𝐴𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) → ∀𝑖𝐴 (𝐹𝑖) ∈ 𝑤)
6321, 62syl 17 . 2 (𝜑 → ∀𝑖𝐴 (𝐹𝑖) ∈ 𝑤)
64 fnfvrnss 7122 . 2 ((𝐹 Fn 𝐴 ∧ ∀𝑖𝐴 (𝐹𝑖) ∈ 𝑤) → ran 𝐹𝑤)
652, 63, 64syl2anc 584 1 (𝜑 → ran 𝐹𝑤)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3061  wrex 3070  Vcvv 3474  cun 3946  wss 3948  {cpr 4630   cuni 4908  cmpt 5231  ran crn 5677   Fn wfn 6538  wf 6539  cfv 6543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-reg 9589
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-eprel 5580  df-fr 5631  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551
This theorem is referenced by:  mnurndlem2  43123
  Copyright terms: Public domain W3C validator