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

Theorem ctmlemr 6986
 Description: Lemma for ctm 6987. 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 6330 . . . . . . . . . 10 ∅ ∈ 1o
2 djurcl 6930 . . . . . . . . . 10 (∅ ∈ 1o → (inr‘∅) ∈ (𝐴 ⊔ 1o))
31, 2ax-mp 5 . . . . . . . . 9 (inr‘∅) ∈ (𝐴 ⊔ 1o)
43a1i 9 . . . . . . . 8 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → (inr‘∅) ∈ (𝐴 ⊔ 1o))
5 simpllr 523 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → 𝑓:ω–onto𝐴)
6 fof 5340 . . . . . . . . . . 11 (𝑓:ω–onto𝐴𝑓:ω⟶𝐴)
75, 6syl 14 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → 𝑓:ω⟶𝐴)
8 nnpredcl 4531 . . . . . . . . . . 11 (𝑛 ∈ ω → 𝑛 ∈ ω)
98ad2antlr 480 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → 𝑛 ∈ ω)
107, 9ffvelrnd 5549 . . . . . . . . 9 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → (𝑓 𝑛) ∈ 𝐴)
11 djulcl 6929 . . . . . . . . 9 ((𝑓 𝑛) ∈ 𝐴 → (inl‘(𝑓 𝑛)) ∈ (𝐴 ⊔ 1o))
1210, 11syl 14 . . . . . . . 8 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → (inl‘(𝑓 𝑛)) ∈ (𝐴 ⊔ 1o))
13 nndceq0 4526 . . . . . . . . 9 (𝑛 ∈ ω → DECID 𝑛 = ∅)
1413adantl 275 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) → DECID 𝑛 = ∅)
154, 12, 14ifcldadc 3496 . . . . . . 7 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) → if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))) ∈ (𝐴 ⊔ 1o))
1615fmpttd 5568 . . . . . 6 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω⟶(𝐴 ⊔ 1o))
17 simpllr 523 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → 𝑓:ω–onto𝐴)
18 simprl 520 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → 𝑤𝐴)
19 foelrn 5647 . . . . . . . . . . 11 ((𝑓:ω–onto𝐴𝑤𝐴) → ∃𝑢 ∈ ω 𝑤 = (𝑓𝑢))
2017, 18, 19syl2anc 408 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → ∃𝑢 ∈ ω 𝑤 = (𝑓𝑢))
21 peano2 4504 . . . . . . . . . . . 12 (𝑢 ∈ ω → suc 𝑢 ∈ ω)
2221ad2antrl 481 . . . . . . . . . . 11 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → suc 𝑢 ∈ ω)
23 simplrr 525 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = (inl‘𝑤))
24 simprl 520 . . . . . . . . . . . . . . . . . . 19 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑢 ∈ ω)
25 nnord 4520 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ω → Ord 𝑢)
26 ordtr 4295 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑢 → Tr 𝑢)
2724, 25, 263syl 17 . . . . . . . . . . . . . . . . . 18 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → Tr 𝑢)
28 unisucg 4331 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ω → (Tr 𝑢 suc 𝑢 = 𝑢))
2928ad2antrl 481 . . . . . . . . . . . . . . . . . 18 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (Tr 𝑢 suc 𝑢 = 𝑢))
3027, 29mpbid 146 . . . . . . . . . . . . . . . . 17 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → suc 𝑢 = 𝑢)
3130fveq2d 5418 . . . . . . . . . . . . . . . 16 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (𝑓 suc 𝑢) = (𝑓𝑢))
32 simprr 521 . . . . . . . . . . . . . . . 16 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑤 = (𝑓𝑢))
3331, 32eqtr4d 2173 . . . . . . . . . . . . . . 15 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (𝑓 suc 𝑢) = 𝑤)
3433fveq2d 5418 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (inl‘(𝑓 suc 𝑢)) = (inl‘𝑤))
3523, 34eqtr4d 2173 . . . . . . . . . . . . 13 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = (inl‘(𝑓 suc 𝑢)))
36 peano3 4505 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ω → suc 𝑢 ≠ ∅)
3736neneqd 2327 . . . . . . . . . . . . . . 15 (𝑢 ∈ ω → ¬ suc 𝑢 = ∅)
3837ad2antrl 481 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → ¬ suc 𝑢 = ∅)
3938iffalsed 3479 . . . . . . . . . . . . 13 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))) = (inl‘(𝑓 suc 𝑢)))
4035, 39eqtr4d 2173 . . . . . . . . . . . 12 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))))
41 eqid 2137 . . . . . . . . . . . . 13 (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))) = (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))
42 eqeq1 2144 . . . . . . . . . . . . . 14 (𝑛 = suc 𝑢 → (𝑛 = ∅ ↔ suc 𝑢 = ∅))
43 unieq 3740 . . . . . . . . . . . . . . . 16 (𝑛 = suc 𝑢 𝑛 = suc 𝑢)
4443fveq2d 5418 . . . . . . . . . . . . . . 15 (𝑛 = suc 𝑢 → (𝑓 𝑛) = (𝑓 suc 𝑢))
4544fveq2d 5418 . . . . . . . . . . . . . 14 (𝑛 = suc 𝑢 → (inl‘(𝑓 𝑛)) = (inl‘(𝑓 suc 𝑢)))
4642, 45ifbieq2d 3491 . . . . . . . . . . . . 13 (𝑛 = suc 𝑢 → if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))) = if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))))
47 simpllr 523 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 ∈ (𝐴 ⊔ 1o))
4840, 47eqeltrrd 2215 . . . . . . . . . . . . 13 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))) ∈ (𝐴 ⊔ 1o))
4941, 46, 22, 48fvmptd3 5507 . . . . . . . . . . . 12 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢) = if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))))
5040, 49eqtr4d 2173 . . . . . . . . . . 11 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢))
51 fveq2 5414 . . . . . . . . . . . 12 (𝑧 = suc 𝑢 → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧) = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢))
5251rspceeqv 2802 . . . . . . . . . . 11 ((suc 𝑢 ∈ ω ∧ 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢)) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
5322, 50, 52syl2anc 408 . . . . . . . . . 10 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
5420, 53rexlimddv 2552 . . . . . . . . 9 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
5554rexlimdvaa 2548 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → (∃𝑤𝐴 𝑦 = (inl‘𝑤) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧)))
56 peano1 4503 . . . . . . . . . 10 ∅ ∈ ω
57 simprr 521 . . . . . . . . . . . . 13 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = (inr‘𝑤))
58 simprl 520 . . . . . . . . . . . . . . 15 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑤 ∈ 1o)
59 el1o 6327 . . . . . . . . . . . . . . 15 (𝑤 ∈ 1o𝑤 = ∅)
6058, 59sylib 121 . . . . . . . . . . . . . 14 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑤 = ∅)
6160fveq2d 5418 . . . . . . . . . . . . 13 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → (inr‘𝑤) = (inr‘∅))
6257, 61eqtrd 2170 . . . . . . . . . . . 12 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = (inr‘∅))
63 eqid 2137 . . . . . . . . . . . . 13 ∅ = ∅
6463iftruei 3475 . . . . . . . . . . . 12 if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) = (inr‘∅)
6562, 64syl6eqr 2188 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
6664, 3eqeltri 2210 . . . . . . . . . . . . 13 if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) ∈ (𝐴 ⊔ 1o)
6766a1i 9 . . . . . . . . . . . 12 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) ∈ (𝐴 ⊔ 1o))
68 eqeq1 2144 . . . . . . . . . . . . . 14 (𝑛 = ∅ → (𝑛 = ∅ ↔ ∅ = ∅))
69 unieq 3740 . . . . . . . . . . . . . . . 16 (𝑛 = ∅ → 𝑛 = ∅)
7069fveq2d 5418 . . . . . . . . . . . . . . 15 (𝑛 = ∅ → (𝑓 𝑛) = (𝑓 ∅))
7170fveq2d 5418 . . . . . . . . . . . . . 14 (𝑛 = ∅ → (inl‘(𝑓 𝑛)) = (inl‘(𝑓 ∅)))
7268, 71ifbieq2d 3491 . . . . . . . . . . . . 13 (𝑛 = ∅ → if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))) = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
7372, 41fvmptg 5490 . . . . . . . . . . . 12 ((∅ ∈ ω ∧ if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) ∈ (𝐴 ⊔ 1o)) → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅) = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
7456, 67, 73sylancr 410 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅) = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
7565, 74eqtr4d 2173 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅))
76 fveq2 5414 . . . . . . . . . . 11 (𝑧 = ∅ → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧) = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅))
7776rspceeqv 2802 . . . . . . . . . 10 ((∅ ∈ ω ∧ 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅)) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
7856, 75, 77sylancr 410 . . . . . . . . 9 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
7978rexlimdvaa 2548 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → (∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧)))
80 djur 6947 . . . . . . . . . 10 (𝑦 ∈ (𝐴 ⊔ 1o) ↔ (∃𝑤𝐴 𝑦 = (inl‘𝑤) ∨ ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤)))
8180biimpi 119 . . . . . . . . 9 (𝑦 ∈ (𝐴 ⊔ 1o) → (∃𝑤𝐴 𝑦 = (inl‘𝑤) ∨ ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤)))
8281adantl 275 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → (∃𝑤𝐴 𝑦 = (inl‘𝑤) ∨ ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤)))
8355, 79, 82mpjaod 707 . . . . . . 7 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
8483ralrimiva 2503 . . . . . 6 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → ∀𝑦 ∈ (𝐴 ⊔ 1o)∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
85 dffo3 5560 . . . . . 6 ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o) ↔ ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω⟶(𝐴 ⊔ 1o) ∧ ∀𝑦 ∈ (𝐴 ⊔ 1o)∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧)))
8616, 84, 85sylanbrc 413 . . . . 5 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o))
87 omex 4502 . . . . . . 7 ω ∈ V
8887mptex 5639 . . . . . 6 (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))) ∈ V
89 foeq1 5336 . . . . . 6 (𝑔 = (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))) → (𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o)))
9088, 89spcev 2775 . . . . 5 ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
9186, 90syl 14 . . . 4 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
9291ex 114 . . 3 (∃𝑥 𝑥𝐴 → (𝑓:ω–onto𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)))
9392exlimdv 1791 . 2 (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)))
94 foeq1 5336 . . 3 (𝑓 = 𝑔 → (𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ 𝑔:ω–onto→(𝐴 ⊔ 1o)))
9594cbvexv 1890 . 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 697  DECID wdc 819   = wceq 1331  ∃wex 1468   ∈ wcel 1480  ∀wral 2414  ∃wrex 2415  ∅c0 3358  ifcif 3469  ∪ cuni 3731   ↦ cmpt 3984  Tr wtr 4021  Ord word 4279  suc csuc 4282  ωcom 4499  ⟶wf 5114  –onto→wfo 5116  ‘cfv 5118  1oc1o 6299   ⊔ cdju 6915  inlcinl 6923  inrcinr 6924 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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-coll 4038  ax-sep 4041  ax-nul 4049  ax-pow 4093  ax-pr 4126  ax-un 4350  ax-iinf 4497 This theorem depends on definitions:  df-bi 116  df-dc 820  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-ral 2419  df-rex 2420  df-reu 2421  df-rab 2423  df-v 2683  df-sbc 2905  df-csb 2999  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-if 3470  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-int 3767  df-iun 3810  df-br 3925  df-opab 3985  df-mpt 3986  df-tr 4022  df-id 4210  df-iord 4283  df-on 4285  df-suc 4288  df-iom 4500  df-xp 4540  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-rn 4545  df-res 4546  df-ima 4547  df-iota 5083  df-fun 5120  df-fn 5121  df-f 5122  df-f1 5123  df-fo 5124  df-f1o 5125  df-fv 5126  df-1st 6031  df-2nd 6032  df-1o 6306  df-dju 6916  df-inl 6925  df-inr 6926 This theorem is referenced by:  ctm  6987
 Copyright terms: Public domain W3C validator