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 42649
Description: Lemma for mnurnd 42651. (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 6670 . 2 (𝜑𝐹 Fn 𝐴)
3 mnurndlem1.6 . . . 4 (𝜑 → ∀𝑖𝐴 (∃𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣 → ∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤)))
4 vex 3448 . . . . . . . 8 𝑖 ∈ V
54prid1 4724 . . . . . . 7 𝑖 ∈ {𝑖, {(𝐹𝑖), 𝐴}}
6 simpr 486 . . . . . . 7 ((𝑖𝐴𝑣 = {𝑖, {(𝐹𝑖), 𝐴}}) → 𝑣 = {𝑖, {(𝐹𝑖), 𝐴}})
75, 6eleqtrrid 2841 . . . . . 6 ((𝑖𝐴𝑣 = {𝑖, {(𝐹𝑖), 𝐴}}) → 𝑖𝑣)
8 eqid 2733 . . . . . . 7 (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}}) = (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})
9 id 22 . . . . . . 7 (𝑖𝐴𝑖𝐴)
10 prex 5390 . . . . . . . 8 {𝑖, {(𝐹𝑖), 𝐴}} ∈ V
1110a1i 11 . . . . . . 7 (𝑖𝐴 → {𝑖, {(𝐹𝑖), 𝐴}} ∈ V)
12 id 22 . . . . . . . . 9 (𝑎 = 𝑖𝑎 = 𝑖)
13 fveq2 6843 . . . . . . . . . 10 (𝑎 = 𝑖 → (𝐹𝑎) = (𝐹𝑖))
1413preq1d 4701 . . . . . . . . 9 (𝑎 = 𝑖 → {(𝐹𝑎), 𝐴} = {(𝐹𝑖), 𝐴})
1512, 14preq12d 4703 . . . . . . . 8 (𝑎 = 𝑖 → {𝑎, {(𝐹𝑎), 𝐴}} = {𝑖, {(𝐹𝑖), 𝐴}})
1615adantl 483 . . . . . . 7 ((𝑖𝐴𝑎 = 𝑖) → {𝑎, {(𝐹𝑎), 𝐴}} = {𝑖, {(𝐹𝑖), 𝐴}})
178, 9, 11, 16rr-elrnmpt3d 42569 . . . . . 6 (𝑖𝐴 → {𝑖, {(𝐹𝑖), 𝐴}} ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}}))
187, 17rspcime 3583 . . . . 5 (𝑖𝐴 → ∃𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣)
1918rgen 3063 . . . 4 𝑖𝐴𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣
20 ralim 3086 . . . 4 (∀𝑖𝐴 (∃𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣 → ∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤)) → (∀𝑖𝐴𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣 → ∀𝑖𝐴𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤)))
213, 19, 20mpisyl 21 . . 3 (𝜑 → ∀𝑖𝐴𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤))
22 prex 5390 . . . . . . . 8 {𝑎, {(𝐹𝑎), 𝐴}} ∈ V
2322rgenw 3065 . . . . . . 7 𝑎𝐴 {𝑎, {(𝐹𝑎), 𝐴}} ∈ V
24 eleq2 2823 . . . . . . . . 9 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → (𝑖𝑢𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}}))
25 unieq 4877 . . . . . . . . . 10 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → 𝑢 = {𝑎, {(𝐹𝑎), 𝐴}})
2625sseq1d 3976 . . . . . . . . 9 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → ( 𝑢𝑤 {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤))
2724, 26anbi12d 632 . . . . . . . 8 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → ((𝑖𝑢 𝑢𝑤) ↔ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)))
288, 27rexrnmptw 7046 . . . . . . 7 (∀𝑎𝐴 {𝑎, {(𝐹𝑎), 𝐴}} ∈ V → (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) ↔ ∃𝑎𝐴 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)))
2923, 28ax-mp 5 . . . . . 6 (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) ↔ ∃𝑎𝐴 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤))
30 simplrl 776 . . . . . . . . . . 11 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → 𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}})
31 simpr 486 . . . . . . . . . . . 12 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → 𝑖𝐴)
32 mnurndlem1.4 . . . . . . . . . . . . . . 15 𝐴 ∈ V
3332prid2 4725 . . . . . . . . . . . . . 14 𝐴 ∈ {(𝐹𝑎), 𝐴}
34 elnotel 9551 . . . . . . . . . . . . . 14 (𝐴 ∈ {(𝐹𝑎), 𝐴} → ¬ {(𝐹𝑎), 𝐴} ∈ 𝐴)
3533, 34ax-mp 5 . . . . . . . . . . . . 13 ¬ {(𝐹𝑎), 𝐴} ∈ 𝐴
3635a1i 11 . . . . . . . . . . . 12 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → ¬ {(𝐹𝑎), 𝐴} ∈ 𝐴)
3731, 36elnelneq2d 42564 . . . . . . . . . . 11 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → ¬ 𝑖 = {(𝐹𝑎), 𝐴})
38 elpri 4609 . . . . . . . . . . . . 13 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} → (𝑖 = 𝑎𝑖 = {(𝐹𝑎), 𝐴}))
3938orcomd 870 . . . . . . . . . . . 12 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} → (𝑖 = {(𝐹𝑎), 𝐴} ∨ 𝑖 = 𝑎))
4039ord 863 . . . . . . . . . . 11 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} → (¬ 𝑖 = {(𝐹𝑎), 𝐴} → 𝑖 = 𝑎))
4130, 37, 40sylc 65 . . . . . . . . . 10 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → 𝑖 = 𝑎)
4241fveq2d 6847 . . . . . . . . 9 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → (𝐹𝑖) = (𝐹𝑎))
43 simplrr 777 . . . . . . . . . 10 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)
44 vex 3448 . . . . . . . . . . . . 13 𝑎 ∈ V
45 prex 5390 . . . . . . . . . . . . 13 {(𝐹𝑎), 𝐴} ∈ V
4644, 45unipr 4884 . . . . . . . . . . . 12 {𝑎, {(𝐹𝑎), 𝐴}} = (𝑎 ∪ {(𝐹𝑎), 𝐴})
4746sseq1i 3973 . . . . . . . . . . 11 ( {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤 ↔ (𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤)
48 unss 4145 . . . . . . . . . . . . 13 ((𝑎𝑤 ∧ {(𝐹𝑎), 𝐴} ⊆ 𝑤) ↔ (𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤)
4948bicomi 223 . . . . . . . . . . . 12 ((𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤 ↔ (𝑎𝑤 ∧ {(𝐹𝑎), 𝐴} ⊆ 𝑤))
5049simprbi 498 . . . . . . . . . . 11 ((𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤 → {(𝐹𝑎), 𝐴} ⊆ 𝑤)
5147, 50sylbi 216 . . . . . . . . . 10 ( {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤 → {(𝐹𝑎), 𝐴} ⊆ 𝑤)
52 fvex 6856 . . . . . . . . . . . . 13 (𝐹𝑎) ∈ V
5352, 32prss 4781 . . . . . . . . . . . 12 (((𝐹𝑎) ∈ 𝑤𝐴𝑤) ↔ {(𝐹𝑎), 𝐴} ⊆ 𝑤)
5453bicomi 223 . . . . . . . . . . 11 ({(𝐹𝑎), 𝐴} ⊆ 𝑤 ↔ ((𝐹𝑎) ∈ 𝑤𝐴𝑤))
5554simplbi 499 . . . . . . . . . 10 ({(𝐹𝑎), 𝐴} ⊆ 𝑤 → (𝐹𝑎) ∈ 𝑤)
5643, 51, 553syl 18 . . . . . . . . 9 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → (𝐹𝑎) ∈ 𝑤)
5742, 56eqeltrd 2834 . . . . . . . 8 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → (𝐹𝑖) ∈ 𝑤)
5857ex 414 . . . . . . 7 ((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) → (𝑖𝐴 → (𝐹𝑖) ∈ 𝑤))
5958rexlimiva 3141 . . . . . 6 (∃𝑎𝐴 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤) → (𝑖𝐴 → (𝐹𝑖) ∈ 𝑤))
6029, 59sylbi 216 . . . . 5 (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) → (𝑖𝐴 → (𝐹𝑖) ∈ 𝑤))
6160com12 32 . . . 4 (𝑖𝐴 → (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) → (𝐹𝑖) ∈ 𝑤))
6261ralimia 3080 . . 3 (∀𝑖𝐴𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) → ∀𝑖𝐴 (𝐹𝑖) ∈ 𝑤)
6321, 62syl 17 . 2 (𝜑 → ∀𝑖𝐴 (𝐹𝑖) ∈ 𝑤)
64 fnfvrnss 7069 . 2 ((𝐹 Fn 𝐴 ∧ ∀𝑖𝐴 (𝐹𝑖) ∈ 𝑤) → ran 𝐹𝑤)
652, 63, 64syl2anc 585 1 (𝜑 → ran 𝐹𝑤)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3061  wrex 3070  Vcvv 3444  cun 3909  wss 3911  {cpr 4589   cuni 4866  cmpt 5189  ran crn 5635   Fn wfn 6492  wf 6493  cfv 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-reg 9533
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-eprel 5538  df-fr 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-fv 6505
This theorem is referenced by:  mnurndlem2  42650
  Copyright terms: Public domain W3C validator