ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fodju0 GIF version

Theorem fodju0 7123
Description: Lemma for fodjuomni 7125 and fodjumkv 7136. A condition which shows that 𝐴 is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
Hypotheses
Ref Expression
fodjuf.fo (𝜑𝐹:𝑂onto→(𝐴𝐵))
fodjuf.p 𝑃 = (𝑦𝑂 ↦ if(∃𝑧𝐴 (𝐹𝑦) = (inl‘𝑧), ∅, 1o))
fodju0.1 (𝜑 → ∀𝑤𝑂 (𝑃𝑤) = 1o)
Assertion
Ref Expression
fodju0 (𝜑𝐴 = ∅)
Distinct variable groups:   𝜑,𝑦,𝑧   𝑦,𝑂,𝑧   𝑧,𝐴   𝑧,𝐵   𝑧,𝐹   𝑦,𝐴   𝑦,𝐹   𝑤,𝑂   𝑤,𝑃
Allowed substitution hints:   𝜑(𝑤)   𝐴(𝑤)   𝐵(𝑦,𝑤)   𝑃(𝑦,𝑧)   𝐹(𝑤)

Proof of Theorem fodju0
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fodjuf.fo . . . . 5 (𝜑𝐹:𝑂onto→(𝐴𝐵))
2 djulcl 7028 . . . . 5 (𝑢𝐴 → (inl‘𝑢) ∈ (𝐴𝐵))
3 foelrn 5732 . . . . 5 ((𝐹:𝑂onto→(𝐴𝐵) ∧ (inl‘𝑢) ∈ (𝐴𝐵)) → ∃𝑣𝑂 (inl‘𝑢) = (𝐹𝑣))
41, 2, 3syl2an 287 . . . 4 ((𝜑𝑢𝐴) → ∃𝑣𝑂 (inl‘𝑢) = (𝐹𝑣))
5 fodjuf.p . . . . . 6 𝑃 = (𝑦𝑂 ↦ if(∃𝑧𝐴 (𝐹𝑦) = (inl‘𝑧), ∅, 1o))
6 fveqeq2 5505 . . . . . . . 8 (𝑦 = 𝑣 → ((𝐹𝑦) = (inl‘𝑧) ↔ (𝐹𝑣) = (inl‘𝑧)))
76rexbidv 2471 . . . . . . 7 (𝑦 = 𝑣 → (∃𝑧𝐴 (𝐹𝑦) = (inl‘𝑧) ↔ ∃𝑧𝐴 (𝐹𝑣) = (inl‘𝑧)))
87ifbid 3547 . . . . . 6 (𝑦 = 𝑣 → if(∃𝑧𝐴 (𝐹𝑦) = (inl‘𝑧), ∅, 1o) = if(∃𝑧𝐴 (𝐹𝑣) = (inl‘𝑧), ∅, 1o))
9 simprl 526 . . . . . 6 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → 𝑣𝑂)
10 peano1 4578 . . . . . . . 8 ∅ ∈ ω
1110a1i 9 . . . . . . 7 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → ∅ ∈ ω)
12 1onn 6499 . . . . . . . 8 1o ∈ ω
1312a1i 9 . . . . . . 7 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → 1o ∈ ω)
141fodjuomnilemdc 7120 . . . . . . . 8 ((𝜑𝑣𝑂) → DECID𝑧𝐴 (𝐹𝑣) = (inl‘𝑧))
1514ad2ant2r 506 . . . . . . 7 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → DECID𝑧𝐴 (𝐹𝑣) = (inl‘𝑧))
1611, 13, 15ifcldcd 3561 . . . . . 6 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → if(∃𝑧𝐴 (𝐹𝑣) = (inl‘𝑧), ∅, 1o) ∈ ω)
175, 8, 9, 16fvmptd3 5589 . . . . 5 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → (𝑃𝑣) = if(∃𝑧𝐴 (𝐹𝑣) = (inl‘𝑧), ∅, 1o))
18 fveqeq2 5505 . . . . . 6 (𝑤 = 𝑣 → ((𝑃𝑤) = 1o ↔ (𝑃𝑣) = 1o))
19 fodju0.1 . . . . . . 7 (𝜑 → ∀𝑤𝑂 (𝑃𝑤) = 1o)
2019ad2antrr 485 . . . . . 6 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → ∀𝑤𝑂 (𝑃𝑤) = 1o)
2118, 20, 9rspcdva 2839 . . . . 5 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → (𝑃𝑣) = 1o)
22 simplr 525 . . . . . . 7 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → 𝑢𝐴)
23 simprr 527 . . . . . . . 8 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → (inl‘𝑢) = (𝐹𝑣))
2423eqcomd 2176 . . . . . . 7 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → (𝐹𝑣) = (inl‘𝑢))
25 fveq2 5496 . . . . . . . 8 (𝑧 = 𝑢 → (inl‘𝑧) = (inl‘𝑢))
2625rspceeqv 2852 . . . . . . 7 ((𝑢𝐴 ∧ (𝐹𝑣) = (inl‘𝑢)) → ∃𝑧𝐴 (𝐹𝑣) = (inl‘𝑧))
2722, 24, 26syl2anc 409 . . . . . 6 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → ∃𝑧𝐴 (𝐹𝑣) = (inl‘𝑧))
2827iftrued 3533 . . . . 5 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → if(∃𝑧𝐴 (𝐹𝑣) = (inl‘𝑧), ∅, 1o) = ∅)
2917, 21, 283eqtr3rd 2212 . . . 4 (((𝜑𝑢𝐴) ∧ (𝑣𝑂 ∧ (inl‘𝑢) = (𝐹𝑣))) → ∅ = 1o)
304, 29rexlimddv 2592 . . 3 ((𝜑𝑢𝐴) → ∅ = 1o)
31 1n0 6411 . . . . 5 1o ≠ ∅
3231nesymi 2386 . . . 4 ¬ ∅ = 1o
3332a1i 9 . . 3 ((𝜑𝑢𝐴) → ¬ ∅ = 1o)
3430, 33pm2.65da 656 . 2 (𝜑 → ¬ 𝑢𝐴)
3534eq0rdv 3459 1 (𝜑𝐴 = ∅)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  DECID wdc 829   = wceq 1348  wcel 2141  wral 2448  wrex 2449  c0 3414  ifcif 3526  cmpt 4050  ωcom 4574  ontowfo 5196  cfv 5198  1oc1o 6388  cdju 7014  inlcinl 7022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-iord 4351  df-on 4353  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-1st 6119  df-2nd 6120  df-1o 6395  df-dju 7015  df-inl 7024  df-inr 7025
This theorem is referenced by:  fodjuomnilemres  7124  fodjumkvlemres  7135
  Copyright terms: Public domain W3C validator