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

Theorem ctmlemr 7136
Description: Lemma for ctm 7137. 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 6464 . . . . . . . . . 10 ∅ ∈ 1o
2 djurcl 7080 . . . . . . . . . 10 (∅ ∈ 1o → (inr‘∅) ∈ (𝐴 ⊔ 1o))
31, 2ax-mp 5 . . . . . . . . 9 (inr‘∅) ∈ (𝐴 ⊔ 1o)
43a1i 9 . . . . . . . 8 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → (inr‘∅) ∈ (𝐴 ⊔ 1o))
5 simpllr 534 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → 𝑓:ω–onto𝐴)
6 fof 5457 . . . . . . . . . . 11 (𝑓:ω–onto𝐴𝑓:ω⟶𝐴)
75, 6syl 14 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → 𝑓:ω⟶𝐴)
8 nnpredcl 4640 . . . . . . . . . . 11 (𝑛 ∈ ω → 𝑛 ∈ ω)
98ad2antlr 489 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → 𝑛 ∈ ω)
107, 9ffvelcdmd 5672 . . . . . . . . 9 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → (𝑓 𝑛) ∈ 𝐴)
11 djulcl 7079 . . . . . . . . 9 ((𝑓 𝑛) ∈ 𝐴 → (inl‘(𝑓 𝑛)) ∈ (𝐴 ⊔ 1o))
1210, 11syl 14 . . . . . . . 8 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) ∧ ¬ 𝑛 = ∅) → (inl‘(𝑓 𝑛)) ∈ (𝐴 ⊔ 1o))
13 nndceq0 4635 . . . . . . . . 9 (𝑛 ∈ ω → DECID 𝑛 = ∅)
1413adantl 277 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) → DECID 𝑛 = ∅)
154, 12, 14ifcldadc 3578 . . . . . . 7 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑛 ∈ ω) → if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))) ∈ (𝐴 ⊔ 1o))
1615fmpttd 5691 . . . . . 6 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω⟶(𝐴 ⊔ 1o))
17 simpllr 534 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → 𝑓:ω–onto𝐴)
18 simprl 529 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → 𝑤𝐴)
19 foelrn 5773 . . . . . . . . . . 11 ((𝑓:ω–onto𝐴𝑤𝐴) → ∃𝑢 ∈ ω 𝑤 = (𝑓𝑢))
2017, 18, 19syl2anc 411 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → ∃𝑢 ∈ ω 𝑤 = (𝑓𝑢))
21 peano2 4612 . . . . . . . . . . . 12 (𝑢 ∈ ω → suc 𝑢 ∈ ω)
2221ad2antrl 490 . . . . . . . . . . 11 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → suc 𝑢 ∈ ω)
23 simplrr 536 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = (inl‘𝑤))
24 simprl 529 . . . . . . . . . . . . . . . . . . 19 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑢 ∈ ω)
25 nnord 4629 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ω → Ord 𝑢)
26 ordtr 4396 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑢 → Tr 𝑢)
2724, 25, 263syl 17 . . . . . . . . . . . . . . . . . 18 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → Tr 𝑢)
28 unisucg 4432 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ω → (Tr 𝑢 suc 𝑢 = 𝑢))
2928ad2antrl 490 . . . . . . . . . . . . . . . . . 18 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (Tr 𝑢 suc 𝑢 = 𝑢))
3027, 29mpbid 147 . . . . . . . . . . . . . . . . 17 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → suc 𝑢 = 𝑢)
3130fveq2d 5538 . . . . . . . . . . . . . . . 16 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (𝑓 suc 𝑢) = (𝑓𝑢))
32 simprr 531 . . . . . . . . . . . . . . . 16 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑤 = (𝑓𝑢))
3331, 32eqtr4d 2225 . . . . . . . . . . . . . . 15 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (𝑓 suc 𝑢) = 𝑤)
3433fveq2d 5538 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → (inl‘(𝑓 suc 𝑢)) = (inl‘𝑤))
3523, 34eqtr4d 2225 . . . . . . . . . . . . 13 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = (inl‘(𝑓 suc 𝑢)))
36 peano3 4613 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ω → suc 𝑢 ≠ ∅)
3736neneqd 2381 . . . . . . . . . . . . . . 15 (𝑢 ∈ ω → ¬ suc 𝑢 = ∅)
3837ad2antrl 490 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → ¬ suc 𝑢 = ∅)
3938iffalsed 3559 . . . . . . . . . . . . 13 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))) = (inl‘(𝑓 suc 𝑢)))
4035, 39eqtr4d 2225 . . . . . . . . . . . 12 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))))
41 eqid 2189 . . . . . . . . . . . . 13 (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))) = (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))
42 eqeq1 2196 . . . . . . . . . . . . . 14 (𝑛 = suc 𝑢 → (𝑛 = ∅ ↔ suc 𝑢 = ∅))
43 unieq 3833 . . . . . . . . . . . . . . . 16 (𝑛 = suc 𝑢 𝑛 = suc 𝑢)
4443fveq2d 5538 . . . . . . . . . . . . . . 15 (𝑛 = suc 𝑢 → (𝑓 𝑛) = (𝑓 suc 𝑢))
4544fveq2d 5538 . . . . . . . . . . . . . 14 (𝑛 = suc 𝑢 → (inl‘(𝑓 𝑛)) = (inl‘(𝑓 suc 𝑢)))
4642, 45ifbieq2d 3573 . . . . . . . . . . . . 13 (𝑛 = suc 𝑢 → if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))) = if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))))
47 simpllr 534 . . . . . . . . . . . . . 14 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 ∈ (𝐴 ⊔ 1o))
4840, 47eqeltrrd 2267 . . . . . . . . . . . . 13 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))) ∈ (𝐴 ⊔ 1o))
4941, 46, 22, 48fvmptd3 5629 . . . . . . . . . . . 12 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢) = if(suc 𝑢 = ∅, (inr‘∅), (inl‘(𝑓 suc 𝑢))))
5040, 49eqtr4d 2225 . . . . . . . . . . 11 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢))
51 fveq2 5534 . . . . . . . . . . . 12 (𝑧 = suc 𝑢 → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧) = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢))
5251rspceeqv 2874 . . . . . . . . . . 11 ((suc 𝑢 ∈ ω ∧ 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘suc 𝑢)) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
5322, 50, 52syl2anc 411 . . . . . . . . . 10 (((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) ∧ (𝑢 ∈ ω ∧ 𝑤 = (𝑓𝑢))) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
5420, 53rexlimddv 2612 . . . . . . . . 9 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤𝐴𝑦 = (inl‘𝑤))) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
5554rexlimdvaa 2608 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → (∃𝑤𝐴 𝑦 = (inl‘𝑤) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧)))
56 peano1 4611 . . . . . . . . . 10 ∅ ∈ ω
57 simprr 531 . . . . . . . . . . . . 13 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = (inr‘𝑤))
58 simprl 529 . . . . . . . . . . . . . . 15 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑤 ∈ 1o)
59 el1o 6461 . . . . . . . . . . . . . . 15 (𝑤 ∈ 1o𝑤 = ∅)
6058, 59sylib 122 . . . . . . . . . . . . . 14 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑤 = ∅)
6160fveq2d 5538 . . . . . . . . . . . . 13 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → (inr‘𝑤) = (inr‘∅))
6257, 61eqtrd 2222 . . . . . . . . . . . 12 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = (inr‘∅))
63 eqid 2189 . . . . . . . . . . . . 13 ∅ = ∅
6463iftruei 3555 . . . . . . . . . . . 12 if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) = (inr‘∅)
6562, 64eqtr4di 2240 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
6664, 3eqeltri 2262 . . . . . . . . . . . . 13 if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) ∈ (𝐴 ⊔ 1o)
6766a1i 9 . . . . . . . . . . . 12 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) ∈ (𝐴 ⊔ 1o))
68 eqeq1 2196 . . . . . . . . . . . . . 14 (𝑛 = ∅ → (𝑛 = ∅ ↔ ∅ = ∅))
69 unieq 3833 . . . . . . . . . . . . . . . 16 (𝑛 = ∅ → 𝑛 = ∅)
7069fveq2d 5538 . . . . . . . . . . . . . . 15 (𝑛 = ∅ → (𝑓 𝑛) = (𝑓 ∅))
7170fveq2d 5538 . . . . . . . . . . . . . 14 (𝑛 = ∅ → (inl‘(𝑓 𝑛)) = (inl‘(𝑓 ∅)))
7268, 71ifbieq2d 3573 . . . . . . . . . . . . 13 (𝑛 = ∅ → if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))) = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
7372, 41fvmptg 5612 . . . . . . . . . . . 12 ((∅ ∈ ω ∧ if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))) ∈ (𝐴 ⊔ 1o)) → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅) = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
7456, 67, 73sylancr 414 . . . . . . . . . . 11 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅) = if(∅ = ∅, (inr‘∅), (inl‘(𝑓 ∅))))
7565, 74eqtr4d 2225 . . . . . . . . . 10 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅))
76 fveq2 5534 . . . . . . . . . . 11 (𝑧 = ∅ → ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧) = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅))
7776rspceeqv 2874 . . . . . . . . . 10 ((∅ ∈ ω ∧ 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘∅)) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
7856, 75, 77sylancr 414 . . . . . . . . 9 ((((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) ∧ (𝑤 ∈ 1o𝑦 = (inr‘𝑤))) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
7978rexlimdvaa 2608 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → (∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧)))
80 djur 7097 . . . . . . . . . 10 (𝑦 ∈ (𝐴 ⊔ 1o) ↔ (∃𝑤𝐴 𝑦 = (inl‘𝑤) ∨ ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤)))
8180biimpi 120 . . . . . . . . 9 (𝑦 ∈ (𝐴 ⊔ 1o) → (∃𝑤𝐴 𝑦 = (inl‘𝑤) ∨ ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤)))
8281adantl 277 . . . . . . . 8 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → (∃𝑤𝐴 𝑦 = (inl‘𝑤) ∨ ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤)))
8355, 79, 82mpjaod 719 . . . . . . 7 (((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) ∧ 𝑦 ∈ (𝐴 ⊔ 1o)) → ∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
8483ralrimiva 2563 . . . . . 6 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → ∀𝑦 ∈ (𝐴 ⊔ 1o)∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧))
85 dffo3 5683 . . . . . 6 ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o) ↔ ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω⟶(𝐴 ⊔ 1o) ∧ ∀𝑦 ∈ (𝐴 ⊔ 1o)∃𝑧 ∈ ω 𝑦 = ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛))))‘𝑧)))
8616, 84, 85sylanbrc 417 . . . . 5 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o))
87 omex 4610 . . . . . . 7 ω ∈ V
8887mptex 5762 . . . . . 6 (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))) ∈ V
89 foeq1 5453 . . . . . 6 (𝑔 = (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))) → (𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ (𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o)))
9088, 89spcev 2847 . . . . 5 ((𝑛 ∈ ω ↦ if(𝑛 = ∅, (inr‘∅), (inl‘(𝑓 𝑛)))):ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
9186, 90syl 14 . . . 4 ((∃𝑥 𝑥𝐴𝑓:ω–onto𝐴) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
9291ex 115 . . 3 (∃𝑥 𝑥𝐴 → (𝑓:ω–onto𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)))
9392exlimdv 1830 . 2 (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)))
94 foeq1 5453 . . 3 (𝑓 = 𝑔 → (𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ 𝑔:ω–onto→(𝐴 ⊔ 1o)))
9594cbvexv 1930 . 2 (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
9693, 95imbitrrdi 162 1 (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto𝐴 → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  DECID wdc 835   = wceq 1364  wex 1503  wcel 2160  wral 2468  wrex 2469  c0 3437  ifcif 3549   cuni 3824  cmpt 4079  Tr wtr 4116  Ord word 4380  suc csuc 4383  ωcom 4607  wf 5231  ontowfo 5233  cfv 5235  1oc1o 6433  cdju 7065  inlcinl 7073  inrcinr 7074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-iinf 4605
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4311  df-iord 4384  df-on 4386  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-1st 6164  df-2nd 6165  df-1o 6440  df-dju 7066  df-inl 7075  df-inr 7076
This theorem is referenced by:  ctm  7137
  Copyright terms: Public domain W3C validator