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

Theorem mnurndlem1 41397
 Description: Lemma for mnurnd 41399. (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 6504 . 2 (𝜑𝐹 Fn 𝐴)
3 mnurndlem1.6 . . . 4 (𝜑 → ∀𝑖𝐴 (∃𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣 → ∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤)))
4 vex 3413 . . . . . . . 8 𝑖 ∈ V
54prid1 4658 . . . . . . 7 𝑖 ∈ {𝑖, {(𝐹𝑖), 𝐴}}
6 simpr 488 . . . . . . 7 ((𝑖𝐴𝑣 = {𝑖, {(𝐹𝑖), 𝐴}}) → 𝑣 = {𝑖, {(𝐹𝑖), 𝐴}})
75, 6eleqtrrid 2859 . . . . . 6 ((𝑖𝐴𝑣 = {𝑖, {(𝐹𝑖), 𝐴}}) → 𝑖𝑣)
8 eqid 2758 . . . . . . 7 (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}}) = (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})
9 id 22 . . . . . . 7 (𝑖𝐴𝑖𝐴)
10 prex 5305 . . . . . . . 8 {𝑖, {(𝐹𝑖), 𝐴}} ∈ V
1110a1i 11 . . . . . . 7 (𝑖𝐴 → {𝑖, {(𝐹𝑖), 𝐴}} ∈ V)
12 id 22 . . . . . . . . 9 (𝑎 = 𝑖𝑎 = 𝑖)
13 fveq2 6663 . . . . . . . . . 10 (𝑎 = 𝑖 → (𝐹𝑎) = (𝐹𝑖))
1413preq1d 4635 . . . . . . . . 9 (𝑎 = 𝑖 → {(𝐹𝑎), 𝐴} = {(𝐹𝑖), 𝐴})
1512, 14preq12d 4637 . . . . . . . 8 (𝑎 = 𝑖 → {𝑎, {(𝐹𝑎), 𝐴}} = {𝑖, {(𝐹𝑖), 𝐴}})
1615adantl 485 . . . . . . 7 ((𝑖𝐴𝑎 = 𝑖) → {𝑎, {(𝐹𝑎), 𝐴}} = {𝑖, {(𝐹𝑖), 𝐴}})
178, 9, 11, 16rr-elrnmpt3d 41322 . . . . . 6 (𝑖𝐴 → {𝑖, {(𝐹𝑖), 𝐴}} ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}}))
187, 17rspcime 3547 . . . . 5 (𝑖𝐴 → ∃𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣)
1918rgen 3080 . . . 4 𝑖𝐴𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣
20 ralim 3094 . . . 4 (∀𝑖𝐴 (∃𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣 → ∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤)) → (∀𝑖𝐴𝑣 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})𝑖𝑣 → ∀𝑖𝐴𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤)))
213, 19, 20mpisyl 21 . . 3 (𝜑 → ∀𝑖𝐴𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤))
22 prex 5305 . . . . . . . 8 {𝑎, {(𝐹𝑎), 𝐴}} ∈ V
2322rgenw 3082 . . . . . . 7 𝑎𝐴 {𝑎, {(𝐹𝑎), 𝐴}} ∈ V
24 eleq2 2840 . . . . . . . . 9 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → (𝑖𝑢𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}}))
25 unieq 4812 . . . . . . . . . 10 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → 𝑢 = {𝑎, {(𝐹𝑎), 𝐴}})
2625sseq1d 3925 . . . . . . . . 9 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → ( 𝑢𝑤 {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤))
2724, 26anbi12d 633 . . . . . . . 8 (𝑢 = {𝑎, {(𝐹𝑎), 𝐴}} → ((𝑖𝑢 𝑢𝑤) ↔ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)))
288, 27rexrnmptw 6858 . . . . . . 7 (∀𝑎𝐴 {𝑎, {(𝐹𝑎), 𝐴}} ∈ V → (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) ↔ ∃𝑎𝐴 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)))
2923, 28ax-mp 5 . . . . . 6 (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) ↔ ∃𝑎𝐴 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤))
30 simplrl 776 . . . . . . . . . . 11 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → 𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}})
31 simpr 488 . . . . . . . . . . . 12 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → 𝑖𝐴)
32 mnurndlem1.4 . . . . . . . . . . . . . . 15 𝐴 ∈ V
3332prid2 4659 . . . . . . . . . . . . . 14 𝐴 ∈ {(𝐹𝑎), 𝐴}
34 elnotel 9119 . . . . . . . . . . . . . 14 (𝐴 ∈ {(𝐹𝑎), 𝐴} → ¬ {(𝐹𝑎), 𝐴} ∈ 𝐴)
3533, 34ax-mp 5 . . . . . . . . . . . . 13 ¬ {(𝐹𝑎), 𝐴} ∈ 𝐴
3635a1i 11 . . . . . . . . . . . 12 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → ¬ {(𝐹𝑎), 𝐴} ∈ 𝐴)
3731, 36elnelneq2d 41317 . . . . . . . . . . 11 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → ¬ 𝑖 = {(𝐹𝑎), 𝐴})
38 elpri 4547 . . . . . . . . . . . . 13 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} → (𝑖 = 𝑎𝑖 = {(𝐹𝑎), 𝐴}))
3938orcomd 868 . . . . . . . . . . . 12 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} → (𝑖 = {(𝐹𝑎), 𝐴} ∨ 𝑖 = 𝑎))
4039ord 861 . . . . . . . . . . 11 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} → (¬ 𝑖 = {(𝐹𝑎), 𝐴} → 𝑖 = 𝑎))
4130, 37, 40sylc 65 . . . . . . . . . 10 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → 𝑖 = 𝑎)
4241fveq2d 6667 . . . . . . . . 9 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → (𝐹𝑖) = (𝐹𝑎))
43 simplrr 777 . . . . . . . . . 10 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)
44 vex 3413 . . . . . . . . . . . . 13 𝑎 ∈ V
45 prex 5305 . . . . . . . . . . . . 13 {(𝐹𝑎), 𝐴} ∈ V
4644, 45unipr 4819 . . . . . . . . . . . 12 {𝑎, {(𝐹𝑎), 𝐴}} = (𝑎 ∪ {(𝐹𝑎), 𝐴})
4746sseq1i 3922 . . . . . . . . . . 11 ( {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤 ↔ (𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤)
48 unss 4091 . . . . . . . . . . . . 13 ((𝑎𝑤 ∧ {(𝐹𝑎), 𝐴} ⊆ 𝑤) ↔ (𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤)
4948bicomi 227 . . . . . . . . . . . 12 ((𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤 ↔ (𝑎𝑤 ∧ {(𝐹𝑎), 𝐴} ⊆ 𝑤))
5049simprbi 500 . . . . . . . . . . 11 ((𝑎 ∪ {(𝐹𝑎), 𝐴}) ⊆ 𝑤 → {(𝐹𝑎), 𝐴} ⊆ 𝑤)
5147, 50sylbi 220 . . . . . . . . . 10 ( {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤 → {(𝐹𝑎), 𝐴} ⊆ 𝑤)
52 fvex 6676 . . . . . . . . . . . . 13 (𝐹𝑎) ∈ V
5352, 32prss 4713 . . . . . . . . . . . 12 (((𝐹𝑎) ∈ 𝑤𝐴𝑤) ↔ {(𝐹𝑎), 𝐴} ⊆ 𝑤)
5453bicomi 227 . . . . . . . . . . 11 ({(𝐹𝑎), 𝐴} ⊆ 𝑤 ↔ ((𝐹𝑎) ∈ 𝑤𝐴𝑤))
5554simplbi 501 . . . . . . . . . 10 ({(𝐹𝑎), 𝐴} ⊆ 𝑤 → (𝐹𝑎) ∈ 𝑤)
5643, 51, 553syl 18 . . . . . . . . 9 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → (𝐹𝑎) ∈ 𝑤)
5742, 56eqeltrd 2852 . . . . . . . 8 (((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖𝐴) → (𝐹𝑖) ∈ 𝑤)
5857ex 416 . . . . . . 7 ((𝑎𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤)) → (𝑖𝐴 → (𝐹𝑖) ∈ 𝑤))
5958rexlimiva 3205 . . . . . 6 (∃𝑎𝐴 (𝑖 ∈ {𝑎, {(𝐹𝑎), 𝐴}} ∧ {𝑎, {(𝐹𝑎), 𝐴}} ⊆ 𝑤) → (𝑖𝐴 → (𝐹𝑖) ∈ 𝑤))
6029, 59sylbi 220 . . . . 5 (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) → (𝑖𝐴 → (𝐹𝑖) ∈ 𝑤))
6160com12 32 . . . 4 (𝑖𝐴 → (∃𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) → (𝐹𝑖) ∈ 𝑤))
6261ralimia 3090 . . 3 (∀𝑖𝐴𝑢 ∈ ran (𝑎𝐴 ↦ {𝑎, {(𝐹𝑎), 𝐴}})(𝑖𝑢 𝑢𝑤) → ∀𝑖𝐴 (𝐹𝑖) ∈ 𝑤)
6321, 62syl 17 . 2 (𝜑 → ∀𝑖𝐴 (𝐹𝑖) ∈ 𝑤)
64 fnfvrnss 6881 . 2 ((𝐹 Fn 𝐴 ∧ ∀𝑖𝐴 (𝐹𝑖) ∈ 𝑤) → ran 𝐹𝑤)
652, 63, 64syl2anc 587 1 (𝜑 → ran 𝐹𝑤)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  Vcvv 3409   ∪ cun 3858   ⊆ wss 3860  {cpr 4527  ∪ cuni 4801   ↦ cmpt 5116  ran crn 5529   Fn wfn 6335  ⟶wf 6336  ‘cfv 6340 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302  ax-reg 9102 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-eprel 5439  df-fr 5487  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-fv 6348 This theorem is referenced by:  mnurndlem2  41398
 Copyright terms: Public domain W3C validator