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

Theorem ctssdclemn0 6945
Description: Lemma for ctssdc 6948. The ¬ ∅ ∈ 𝑆 case. (Contributed by Jim Kingdon, 16-Aug-2023.)
Hypotheses
Ref Expression
ctssdclemn0.ss (𝜑𝑆 ⊆ ω)
ctssdclemn0.dc (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)
ctssdclemn0.f (𝜑𝐹:𝑆onto𝐴)
ctssdclemn0.n0 (𝜑 → ¬ ∅ ∈ 𝑆)
Assertion
Ref Expression
ctssdclemn0 (𝜑 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
Distinct variable groups:   𝐴,𝑔   𝑔,𝐹   𝑆,𝑔   𝑆,𝑛
Allowed substitution hints:   𝜑(𝑔,𝑛)   𝐴(𝑛)   𝐹(𝑛)

Proof of Theorem ctssdclemn0
Dummy variables 𝑚 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ctssdclemn0.f . . . . . . . . 9 (𝜑𝐹:𝑆onto𝐴)
21ad2antrr 477 . . . . . . . 8 (((𝜑𝑚 ∈ ω) ∧ 𝑚𝑆) → 𝐹:𝑆onto𝐴)
3 fof 5301 . . . . . . . 8 (𝐹:𝑆onto𝐴𝐹:𝑆𝐴)
42, 3syl 14 . . . . . . 7 (((𝜑𝑚 ∈ ω) ∧ 𝑚𝑆) → 𝐹:𝑆𝐴)
5 simpr 109 . . . . . . 7 (((𝜑𝑚 ∈ ω) ∧ 𝑚𝑆) → 𝑚𝑆)
64, 5ffvelrnd 5508 . . . . . 6 (((𝜑𝑚 ∈ ω) ∧ 𝑚𝑆) → (𝐹𝑚) ∈ 𝐴)
7 djulcl 6886 . . . . . 6 ((𝐹𝑚) ∈ 𝐴 → (inl‘(𝐹𝑚)) ∈ (𝐴 ⊔ 1o))
86, 7syl 14 . . . . 5 (((𝜑𝑚 ∈ ω) ∧ 𝑚𝑆) → (inl‘(𝐹𝑚)) ∈ (𝐴 ⊔ 1o))
9 0lt1o 6289 . . . . . . 7 ∅ ∈ 1o
10 djurcl 6887 . . . . . . 7 (∅ ∈ 1o → (inr‘∅) ∈ (𝐴 ⊔ 1o))
119, 10ax-mp 7 . . . . . 6 (inr‘∅) ∈ (𝐴 ⊔ 1o)
1211a1i 9 . . . . 5 (((𝜑𝑚 ∈ ω) ∧ ¬ 𝑚𝑆) → (inr‘∅) ∈ (𝐴 ⊔ 1o))
13 eleq1 2175 . . . . . . 7 (𝑛 = 𝑚 → (𝑛𝑆𝑚𝑆))
1413dcbid 806 . . . . . 6 (𝑛 = 𝑚 → (DECID 𝑛𝑆DECID 𝑚𝑆))
15 ctssdclemn0.dc . . . . . . 7 (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)
1615adantr 272 . . . . . 6 ((𝜑𝑚 ∈ ω) → ∀𝑛 ∈ ω DECID 𝑛𝑆)
17 simpr 109 . . . . . 6 ((𝜑𝑚 ∈ ω) → 𝑚 ∈ ω)
1814, 16, 17rspcdva 2763 . . . . 5 ((𝜑𝑚 ∈ ω) → DECID 𝑚𝑆)
198, 12, 18ifcldadc 3465 . . . 4 ((𝜑𝑚 ∈ ω) → if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)) ∈ (𝐴 ⊔ 1o))
2019fmpttd 5527 . . 3 (𝜑 → (𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅))):ω⟶(𝐴 ⊔ 1o))
211ad3antrrr 481 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) → 𝐹:𝑆onto𝐴)
22 simplr 502 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) → 𝑧𝐴)
23 foelrn 5606 . . . . . . . . 9 ((𝐹:𝑆onto𝐴𝑧𝐴) → ∃𝑦𝑆 𝑧 = (𝐹𝑦))
2421, 22, 23syl2anc 406 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) → ∃𝑦𝑆 𝑧 = (𝐹𝑦))
25 simplr 502 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → 𝑦𝑆)
2625iftrued 3445 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → if(𝑦𝑆, (inl‘(𝐹𝑦)), (inr‘∅)) = (inl‘(𝐹𝑦)))
27 eqid 2113 . . . . . . . . . . . 12 (𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅))) = (𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))
28 eleq1 2175 . . . . . . . . . . . . 13 (𝑚 = 𝑦 → (𝑚𝑆𝑦𝑆))
29 2fveq3 5378 . . . . . . . . . . . . 13 (𝑚 = 𝑦 → (inl‘(𝐹𝑚)) = (inl‘(𝐹𝑦)))
3028, 29ifbieq1d 3458 . . . . . . . . . . . 12 (𝑚 = 𝑦 → if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)) = if(𝑦𝑆, (inl‘(𝐹𝑦)), (inr‘∅)))
31 ctssdclemn0.ss . . . . . . . . . . . . . 14 (𝜑𝑆 ⊆ ω)
3231ad5antr 485 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → 𝑆 ⊆ ω)
3332, 25sseldd 3062 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → 𝑦 ∈ ω)
341, 3syl 14 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑆𝐴)
3534ad5antr 485 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → 𝐹:𝑆𝐴)
3635, 25ffvelrnd 5508 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → (𝐹𝑦) ∈ 𝐴)
37 djulcl 6886 . . . . . . . . . . . . . 14 ((𝐹𝑦) ∈ 𝐴 → (inl‘(𝐹𝑦)) ∈ (𝐴 ⊔ 1o))
3836, 37syl 14 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → (inl‘(𝐹𝑦)) ∈ (𝐴 ⊔ 1o))
3926, 38eqeltrd 2189 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → if(𝑦𝑆, (inl‘(𝐹𝑦)), (inr‘∅)) ∈ (𝐴 ⊔ 1o))
4027, 30, 33, 39fvmptd3 5466 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦) = if(𝑦𝑆, (inl‘(𝐹𝑦)), (inr‘∅)))
41 simpllr 506 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = (inl‘𝑧))
42 simpr 109 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → 𝑧 = (𝐹𝑦))
4342fveq2d 5377 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → (inl‘𝑧) = (inl‘(𝐹𝑦)))
4441, 43eqtrd 2145 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = (inl‘(𝐹𝑦)))
4526, 40, 443eqtr4rd 2156 . . . . . . . . . 10 ((((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦))
4645ex 114 . . . . . . . . 9 (((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) ∧ 𝑦𝑆) → (𝑧 = (𝐹𝑦) → 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦)))
4746reximdva 2506 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) → (∃𝑦𝑆 𝑧 = (𝐹𝑦) → ∃𝑦𝑆 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦)))
4824, 47mpd 13 . . . . . . 7 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) → ∃𝑦𝑆 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦))
49 ssrexv 3126 . . . . . . . . 9 (𝑆 ⊆ ω → (∃𝑦𝑆 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦) → ∃𝑦 ∈ ω 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦)))
5031, 49syl 14 . . . . . . . 8 (𝜑 → (∃𝑦𝑆 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦) → ∃𝑦 ∈ ω 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦)))
5150ad3antrrr 481 . . . . . . 7 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) → (∃𝑦𝑆 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦) → ∃𝑦 ∈ ω 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦)))
5248, 51mpd 13 . . . . . 6 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧𝐴) ∧ 𝑥 = (inl‘𝑧)) → ∃𝑦 ∈ ω 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦))
5352rexlimdva2 2524 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) → (∃𝑧𝐴 𝑥 = (inl‘𝑧) → ∃𝑦 ∈ ω 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦)))
54 peano1 4466 . . . . . . . 8 ∅ ∈ ω
5554a1i 9 . . . . . . 7 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → ∅ ∈ ω)
56 ctssdclemn0.n0 . . . . . . . . . 10 (𝜑 → ¬ ∅ ∈ 𝑆)
5756ad3antrrr 481 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → ¬ ∅ ∈ 𝑆)
5857iffalsed 3448 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → if(∅ ∈ 𝑆, (inl‘(𝐹‘∅)), (inr‘∅)) = (inr‘∅))
59 eleq1 2175 . . . . . . . . . 10 (𝑚 = ∅ → (𝑚𝑆 ↔ ∅ ∈ 𝑆))
60 2fveq3 5378 . . . . . . . . . 10 (𝑚 = ∅ → (inl‘(𝐹𝑚)) = (inl‘(𝐹‘∅)))
6159, 60ifbieq1d 3458 . . . . . . . . 9 (𝑚 = ∅ → if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)) = if(∅ ∈ 𝑆, (inl‘(𝐹‘∅)), (inr‘∅)))
6258, 11syl6eqel 2203 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → if(∅ ∈ 𝑆, (inl‘(𝐹‘∅)), (inr‘∅)) ∈ (𝐴 ⊔ 1o))
6327, 61, 55, 62fvmptd3 5466 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘∅) = if(∅ ∈ 𝑆, (inl‘(𝐹‘∅)), (inr‘∅)))
64 simpr 109 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → 𝑥 = (inr‘𝑧))
65 simplr 502 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → 𝑧 ∈ 1o)
66 el1o 6286 . . . . . . . . . . 11 (𝑧 ∈ 1o𝑧 = ∅)
6765, 66sylib 121 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → 𝑧 = ∅)
6867fveq2d 5377 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → (inr‘𝑧) = (inr‘∅))
6964, 68eqtrd 2145 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → 𝑥 = (inr‘∅))
7058, 63, 693eqtr4rd 2156 . . . . . . 7 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘∅))
71 fveq2 5373 . . . . . . . 8 (𝑦 = ∅ → ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦) = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘∅))
7271rspceeqv 2775 . . . . . . 7 ((∅ ∈ ω ∧ 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘∅)) → ∃𝑦 ∈ ω 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦))
7355, 70, 72syl2anc 406 . . . . . 6 ((((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) ∧ 𝑧 ∈ 1o) ∧ 𝑥 = (inr‘𝑧)) → ∃𝑦 ∈ ω 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦))
7473rexlimdva2 2524 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) → (∃𝑧 ∈ 1o 𝑥 = (inr‘𝑧) → ∃𝑦 ∈ ω 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦)))
75 djur 6904 . . . . . . 7 (𝑥 ∈ (𝐴 ⊔ 1o) ↔ (∃𝑧𝐴 𝑥 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑥 = (inr‘𝑧)))
7675biimpi 119 . . . . . 6 (𝑥 ∈ (𝐴 ⊔ 1o) → (∃𝑧𝐴 𝑥 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑥 = (inr‘𝑧)))
7776adantl 273 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) → (∃𝑧𝐴 𝑥 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑥 = (inr‘𝑧)))
7853, 74, 77mpjaod 690 . . . 4 ((𝜑𝑥 ∈ (𝐴 ⊔ 1o)) → ∃𝑦 ∈ ω 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦))
7978ralrimiva 2477 . . 3 (𝜑 → ∀𝑥 ∈ (𝐴 ⊔ 1o)∃𝑦 ∈ ω 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦))
80 dffo3 5519 . . 3 ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅))):ω–onto→(𝐴 ⊔ 1o) ↔ ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅))):ω⟶(𝐴 ⊔ 1o) ∧ ∀𝑥 ∈ (𝐴 ⊔ 1o)∃𝑦 ∈ ω 𝑥 = ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅)))‘𝑦)))
8120, 79, 80sylanbrc 411 . 2 (𝜑 → (𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅))):ω–onto→(𝐴 ⊔ 1o))
82 omex 4465 . . . 4 ω ∈ V
8382mptex 5598 . . 3 (𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅))) ∈ V
84 foeq1 5297 . . 3 (𝑔 = (𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅))) → (𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ (𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅))):ω–onto→(𝐴 ⊔ 1o)))
8583, 84spcev 2749 . 2 ((𝑚 ∈ ω ↦ if(𝑚𝑆, (inl‘(𝐹𝑚)), (inr‘∅))):ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
8681, 85syl 14 1 (𝜑 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 680  DECID wdc 802   = wceq 1312  wex 1449  wcel 1461  wral 2388  wrex 2389  wss 3035  c0 3327  ifcif 3438  cmpt 3947  ωcom 4462  wf 5075  ontowfo 5077  cfv 5079  1oc1o 6258  cdju 6872  inlcinl 6880  inrcinr 6881
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 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-coll 4001  ax-sep 4004  ax-nul 4012  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-iinf 4460
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-reu 2395  df-rab 2397  df-v 2657  df-sbc 2877  df-csb 2970  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-nul 3328  df-if 3439  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-iun 3779  df-br 3894  df-opab 3948  df-mpt 3949  df-tr 3985  df-id 4173  df-iord 4246  df-on 4248  df-suc 4251  df-iom 4463  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-f1 5084  df-fo 5085  df-f1o 5086  df-fv 5087  df-1st 5990  df-2nd 5991  df-1o 6265  df-dju 6873  df-inl 6882  df-inr 6883
This theorem is referenced by:  ctssdc  6948
  Copyright terms: Public domain W3C validator