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

Theorem ctmlemr 6870
Description: Lemma for ctm 6871. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.)
Assertion
Ref Expression
ctmlemr (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto𝐴 → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o)))
Distinct variable groups:   𝐴,𝑓   𝑥,𝑓
Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem ctmlemr
Dummy variables 𝑔 𝑛 𝑢 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0lt1o 6242 . . . . . . . . . 10 ∅ ∈ 1o
2 djurcl 6824 . . . . . . . . . 10 (∅ ∈ 1o → (inr‘∅) ∈ (𝐴 ⊔ 1o))
31, 2ax-mp 7 . . . . . . . . 9 (inr‘∅) ∈ (𝐴 ⊔ 1o)
43a1i 9 . . . . . . . 8 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → (inr‘∅) ∈ (𝐴 ⊔ 1o))
5 simpllr 502 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → 𝑓:ω–onto𝐴)
6 fof 5268 . . . . . . . . . . 11 (𝑓:ω–onto𝐴𝑓:ω⟶𝐴)
75, 6syl 14 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → 𝑓:ω⟶𝐴)
8 nnpredcl 4464 . . . . . . . . . . 11 (𝑛 ∈ ω → 𝑛 ∈ ω)
98ad2antlr 474 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → 𝑛 ∈ ω)
107, 9ffvelrnd 5474 . . . . . . . . 9 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → (𝑓 𝑛) ∈ 𝐴)
11 djulcl 6823 . . . . . . . . 9 ((𝑓 𝑛) ∈ 𝐴 → (inl‘(𝑓 𝑛)) ∈ (𝐴 ⊔ 1o))
1210, 11syl 14 . . . . . . . 8 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → (inl‘(𝑓 𝑛)) ∈ (𝐴 ⊔ 1o))
13 nndceq0 4459 . . . . . . . . 9 (𝑛 ∈ ω → DECID 𝑛 = ∅)
1413adantl 272 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) → DECID 𝑛 = ∅)
154, 12, 14ifcldadc 3440 . . . . . . 7 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) → if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))) ∈ (𝐴 ⊔ 1o))
1615fmpttd 5492 . . . . . 6 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω⟶(𝐴 ⊔ 1o))
17 simpllr 502 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → 𝑓:ω–onto𝐴)
18 simprl 499 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → 𝑤𝐴)
19 foelrn 5570 . . . . . . . . . . 11 ((𝑓:ω–onto𝐴𝑤𝐴) → ∃𝑢 ∈ ω 𝑤 = (𝑓𝑢))
2017, 18, 19syl2anc 404 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → ∃𝑢 ∈ ω 𝑤 = (𝑓𝑢))
21 peano2 4438 . . . . . . . . . . . 12 (𝑢 ∈ ω → suc 𝑢 ∈ ω)
2221ad2antrl 475 . . . . . . . . . . 11 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → suc 𝑢 ∈ ω)
23 simplrr 504 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = (inl‘𝑤))
24 simprl 499 . . . . . . . . . . . . . . . . . . 19 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑢 ∈ ω)
25 nnord 4454 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ω → Ord 𝑢)
26 ordtr 4229 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑢 → Tr 𝑢)
2724, 25, 263syl 17 . . . . . . . . . . . . . . . . . 18 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → Tr 𝑢)
28 unisucg 4265 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ω → (Tr 𝑢 suc 𝑢 = 𝑢))
2928ad2antrl 475 . . . . . . . . . . . . . . . . . 18 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (Tr 𝑢 suc 𝑢 = 𝑢))
3027, 29mpbid 146 . . . . . . . . . . . . . . . . 17 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → suc 𝑢 = 𝑢)
3130fveq2d 5344 . . . . . . . . . . . . . . . 16 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (𝑓 suc 𝑢) = (𝑓𝑢))
32 simprr 500 . . . . . . . . . . . . . . . 16 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑤 = (𝑓𝑢))
3331, 32eqtr4d 2130 . . . . . . . . . . . . . . 15 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (𝑓 suc 𝑢) = 𝑤)
3433fveq2d 5344 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (inl‘(𝑓 suc 𝑢)) = (inl‘𝑤))
3523, 34eqtr4d 2130 . . . . . . . . . . . . 13 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = (inl‘(𝑓 suc 𝑢)))
36 peano3 4439 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ω → suc 𝑢 ≠ ∅)
3736neneqd 2283 . . . . . . . . . . . . . . 15 (𝑢 ∈ ω → ¬ suc 𝑢 = ∅)
3837ad2antrl 475 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → ¬ suc 𝑢 = ∅)
3938iffalsed 3423 . . . . . . . . . . . . 13 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))) = (inl‘(𝑓 suc 𝑢)))
4035, 39eqtr4d 2130 . . . . . . . . . . . 12 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))))
41 simpllr 502 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 ∈ (𝐴 ⊔ 1o))
4240, 41eqeltrrd 2172 . . . . . . . . . . . . 13 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))) ∈ (𝐴 ⊔ 1o))
43 eqeq1 2101 . . . . . . . . . . . . . . 15 (𝑛 = suc 𝑢 → (𝑛 = ∅ ↔ suc 𝑢 = ∅))
44 unieq 3684 . . . . . . . . . . . . . . . . 17 (𝑛 = suc 𝑢 𝑛 = suc 𝑢)
4544fveq2d 5344 . . . . . . . . . . . . . . . 16 (𝑛 = suc 𝑢 → (𝑓 𝑛) = (𝑓 suc 𝑢))
4645fveq2d 5344 . . . . . . . . . . . . . . 15 (𝑛 = suc 𝑢 → (inl‘(𝑓 𝑛)) = (inl‘(𝑓 suc 𝑢)))
4743, 46ifbieq2d 3435 . . . . . . . . . . . . . 14 (𝑛 = suc 𝑢 → if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))) = if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))))
48 eqid 2095 . . . . . . . . . . . . . 14 (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))) = (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))
4947, 48fvmptg 5415 . . . . . . . . . . . . 13 ((suc 𝑢 ∈ ω ∧ if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))) ∈ (𝐴 ⊔ 1o)) → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢) = if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))))
5022, 42, 49syl2anc 404 . . . . . . . . . . . 12 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢) = if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))))
5140, 50eqtr4d 2130 . . . . . . . . . . 11 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢))
52 fveq2 5340 . . . . . . . . . . . 12 (𝑧 = suc 𝑢 → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧) = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢))
5352rspceeqv 2753 . . . . . . . . . . 11 ((suc 𝑢 ∈ ω ∧ 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢)) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
5422, 51, 53syl2anc 404 . . . . . . . . . 10 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
5520, 54rexlimddv 2507 . . . . . . . . 9 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
5655rexlimdvaa 2503 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → (∃𝑤𝐴 𝑦 = (inl‘𝑤) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧)))
57 peano1 4437 . . . . . . . . . 10 ∅ ∈ ω
58 simprr 500 . . . . . . . . . . . . 13 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = (inr‘𝑤))
59 simprl 499 . . . . . . . . . . . . . . 15 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑤 ∈ 1o)
60 el1o 6239 . . . . . . . . . . . . . . 15 (𝑤 ∈ 1o𝑤 = ∅)
6159, 60sylib 121 . . . . . . . . . . . . . 14 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑤 = ∅)
6261fveq2d 5344 . . . . . . . . . . . . 13 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → (inr‘𝑤) = (inr‘∅))
6358, 62eqtrd 2127 . . . . . . . . . . . 12 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = (inr‘∅))
64 eqid 2095 . . . . . . . . . . . . 13 ∅ = ∅
6564iftruei 3419 . . . . . . . . . . . 12 if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) = (inr‘∅)
6663, 65syl6eqr 2145 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
6765, 3eqeltri 2167 . . . . . . . . . . . . 13 if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) ∈ (𝐴 ⊔ 1o)
6867a1i 9 . . . . . . . . . . . 12 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) ∈ (𝐴 ⊔ 1o))
69 eqeq1 2101 . . . . . . . . . . . . . 14 (𝑛 = ∅ → (𝑛 = ∅ ↔ ∅ = ∅))
70 unieq 3684 . . . . . . . . . . . . . . . 16 (𝑛 = ∅ → 𝑛 = ∅)
7170fveq2d 5344 . . . . . . . . . . . . . . 15 (𝑛 = ∅ → (𝑓 𝑛) = (𝑓 ∅))
7271fveq2d 5344 . . . . . . . . . . . . . 14 (𝑛 = ∅ → (inl‘(𝑓 𝑛)) = (inl‘(𝑓 ∅)))
7369, 72ifbieq2d 3435 . . . . . . . . . . . . 13 (𝑛 = ∅ → if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))) = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
7473, 48fvmptg 5415 . . . . . . . . . . . 12 ((∅ ∈ ω ∧ if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) ∈ (𝐴 ⊔ 1o)) → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅) = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
7557, 68, 74sylancr 406 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅) = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
7666, 75eqtr4d 2130 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅))
77 fveq2 5340 . . . . . . . . . . 11 (𝑧 = ∅ → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧) = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅))
7877rspceeqv 2753 . . . . . . . . . 10 ((∅ ∈ ω ∧ 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅)) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
7957, 76, 78sylancr 406 . . . . . . . . 9 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
8079rexlimdvaa 2503 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → (∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧)))
81 djur 6837 . . . . . . . . 9 (𝑦 ∈ (𝐴 ⊔ 1o) → (∃𝑤𝐴 𝑦 = (inl‘𝑤) ∨ ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤)))
8281adantl 272 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → (∃𝑤𝐴 𝑦 = (inl‘𝑤) ∨ ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤)))
8356, 80, 82mpjaod 676 . . . . . . 7 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
8483ralrimiva 2458 . . . . . 6 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → ∀𝑦 ∈ (𝐴 ⊔ 1o)∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
85 dffo3 5485 . . . . . 6 ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o) ↔ ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω⟶(𝐴 ⊔ 1o) ∧ ∀𝑦 ∈ (𝐴 ⊔ 1o)∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧)))
8616, 84, 85sylanbrc 409 . . . . 5 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o))
87 omex 4436 . . . . . . 7 ω ∈ V
8887mptex 5562 . . . . . 6 (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))) ∈ V
89 foeq1 5264 . . . . . 6 (𝑔 = (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))) → (𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o)))
9088, 89spcev 2727 . . . . 5 ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
9186, 90syl 14 . . . 4 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
9291ex 114 . . 3 (∃𝑥 𝑥𝐴 → (𝑓:ω–onto𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)))
9392exlimdv 1754 . 2 (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)))
94 foeq1 5264 . . 3 (𝑓 = 𝑔 → (𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ 𝑔:ω–onto→(𝐴 ⊔ 1o)))
9594cbvexv 1850 . 2 (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
9693, 95syl6ibr 161 1 (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto𝐴 → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 667  DECID wdc 783   = wceq 1296  wex 1433  wcel 1445  wral 2370  wrex 2371  c0 3302  ifcif 3413   cuni 3675  cmpt 3921  Tr wtr 3958  Ord word 4213  suc csuc 4216  ωcom 4433  wf 5045  ontowfo 5047  cfv 5049  1oc1o 6212  cdju 6810  inlcinl 6817  inrcinr 6818
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-coll 3975  ax-sep 3978  ax-nul 3986  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-iinf 4431
This theorem depends on definitions:  df-bi 116  df-dc 784  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-csb 2948  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-nul 3303  df-if 3414  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-iun 3754  df-br 3868  df-opab 3922  df-mpt 3923  df-tr 3959  df-id 4144  df-iord 4217  df-on 4219  df-suc 4222  df-iom 4434  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-rn 4478  df-res 4479  df-ima 4480  df-iota 5014  df-fun 5051  df-fn 5052  df-f 5053  df-f1 5054  df-fo 5055  df-f1o 5056  df-fv 5057  df-1st 5949  df-2nd 5950  df-1o 6219  df-dju 6811  df-inl 6819  df-inr 6820
This theorem is referenced by:  ctm  6871
  Copyright terms: Public domain W3C validator