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

Theorem modelaxreplem1 44942
Description: Lemma for modelaxrep 44945. We show that 𝑀 is closed under taking subsets. (Contributed by Eric Schmidt, 29-Sep-2025.)
Hypotheses
Ref Expression
modelaxreplem.1 (𝜓𝑥𝑀)
modelaxreplem.2 (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) → ran 𝑓𝑀))
modelaxreplem.3 (𝜓 → ∅ ∈ 𝑀)
modelaxreplem.4 (𝜓𝑥𝑀)
modelaxreplem1.5 𝐴𝑥
Assertion
Ref Expression
modelaxreplem1 (𝜓𝐴𝑀)
Distinct variable group:   𝑓,𝑀
Allowed substitution hints:   𝜓(𝑥,𝑓)   𝐴(𝑥,𝑓)   𝑀(𝑥)

Proof of Theorem modelaxreplem1
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 modelaxreplem.3 . . 3 (𝜓 → ∅ ∈ 𝑀)
2 eleq1 2826 . . 3 (𝐴 = ∅ → (𝐴𝑀 ↔ ∅ ∈ 𝑀))
31, 2syl5ibrcom 247 . 2 (𝜓 → (𝐴 = ∅ → 𝐴𝑀))
4 vex 3481 . . . . . 6 𝑥 ∈ V
5 modelaxreplem1.5 . . . . . 6 𝐴𝑥
64, 5ssexi 5327 . . . . 5 𝐴 ∈ V
760sdom 9145 . . . 4 (∅ ≺ 𝐴𝐴 ≠ ∅)
8 ssdomg 9038 . . . . . 6 (𝑥 ∈ V → (𝐴𝑥𝐴𝑥))
94, 5, 8mp2 9 . . . . 5 𝐴𝑥
10 fodomr 9166 . . . . 5 ((∅ ≺ 𝐴𝐴𝑥) → ∃𝑔 𝑔:𝑥onto𝐴)
119, 10mpan2 691 . . . 4 (∅ ≺ 𝐴 → ∃𝑔 𝑔:𝑥onto𝐴)
127, 11sylbir 235 . . 3 (𝐴 ≠ ∅ → ∃𝑔 𝑔:𝑥onto𝐴)
13 df-fo 6568 . . . . 5 (𝑔:𝑥onto𝐴 ↔ (𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴))
14 df-fn 6565 . . . . . . . 8 (𝑔 Fn 𝑥 ↔ (Fun 𝑔 ∧ dom 𝑔 = 𝑥))
15 modelaxreplem.4 . . . . . . . . . 10 (𝜓𝑥𝑀)
16 eleq1 2826 . . . . . . . . . 10 (dom 𝑔 = 𝑥 → (dom 𝑔𝑀𝑥𝑀))
1715, 16syl5ibrcom 247 . . . . . . . . 9 (𝜓 → (dom 𝑔 = 𝑥 → dom 𝑔𝑀))
1817anim2d 612 . . . . . . . 8 (𝜓 → ((Fun 𝑔 ∧ dom 𝑔 = 𝑥) → (Fun 𝑔 ∧ dom 𝑔𝑀)))
1914, 18biimtrid 242 . . . . . . 7 (𝜓 → (𝑔 Fn 𝑥 → (Fun 𝑔 ∧ dom 𝑔𝑀)))
20 modelaxreplem.1 . . . . . . . . 9 (𝜓𝑥𝑀)
215, 20sstrid 4006 . . . . . . . 8 (𝜓𝐴𝑀)
22 sseq1 4020 . . . . . . . 8 (ran 𝑔 = 𝐴 → (ran 𝑔𝑀𝐴𝑀))
2321, 22syl5ibrcom 247 . . . . . . 7 (𝜓 → (ran 𝑔 = 𝐴 → ran 𝑔𝑀))
24 df-3an 1088 . . . . . . . 8 ((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) ↔ ((Fun 𝑔 ∧ dom 𝑔𝑀) ∧ ran 𝑔𝑀))
25 modelaxreplem.2 . . . . . . . . 9 (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) → ran 𝑓𝑀))
26 funeq 6587 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
27 dmeq 5916 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔)
2827eleq1d 2823 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (dom 𝑓𝑀 ↔ dom 𝑔𝑀))
29 rneq 5949 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → ran 𝑓 = ran 𝑔)
3029sseq1d 4026 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (ran 𝑓𝑀 ↔ ran 𝑔𝑀))
3126, 28, 303anbi123d 1435 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) ↔ (Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀)))
3229eleq1d 2823 . . . . . . . . . . 11 (𝑓 = 𝑔 → (ran 𝑓𝑀 ↔ ran 𝑔𝑀))
3331, 32imbi12d 344 . . . . . . . . . 10 (𝑓 = 𝑔 → (((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) → ran 𝑓𝑀) ↔ ((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)))
3433spvv 1993 . . . . . . . . 9 (∀𝑓((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) → ran 𝑓𝑀) → ((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀))
3525, 34syl 17 . . . . . . . 8 (𝜓 → ((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀))
3624, 35biimtrrid 243 . . . . . . 7 (𝜓 → (((Fun 𝑔 ∧ dom 𝑔𝑀) ∧ ran 𝑔𝑀) → ran 𝑔𝑀))
3719, 23, 36syl2and 608 . . . . . 6 (𝜓 → ((𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴) → ran 𝑔𝑀))
38 eleq1 2826 . . . . . . 7 (ran 𝑔 = 𝐴 → (ran 𝑔𝑀𝐴𝑀))
3938adantl 481 . . . . . 6 ((𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴) → (ran 𝑔𝑀𝐴𝑀))
4037, 39mpbidi 241 . . . . 5 (𝜓 → ((𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴) → 𝐴𝑀))
4113, 40biimtrid 242 . . . 4 (𝜓 → (𝑔:𝑥onto𝐴𝐴𝑀))
4241exlimdv 1930 . . 3 (𝜓 → (∃𝑔 𝑔:𝑥onto𝐴𝐴𝑀))
4312, 42syl5 34 . 2 (𝜓 → (𝐴 ≠ ∅ → 𝐴𝑀))
443, 43pm2.61dne 3025 1 (𝜓𝐴𝑀)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086  wal 1534   = wceq 1536  wex 1775  wcel 2105  wne 2937  Vcvv 3477  wss 3962  c0 4338   class class class wbr 5147  dom cdm 5688  ran crn 5689  Fun wfun 6556   Fn wfn 6557  ontowfo 6560  cdom 8981  csdm 8982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-en 8984  df-dom 8985  df-sdom 8986
This theorem is referenced by:  modelaxreplem2  44943
  Copyright terms: Public domain W3C validator