Theorem ctiunctlemuom 11985

Description: Lemma for ctiunct 11989. (Contributed by Jim Kingdon, 28-Oct-2023.)

Hypotheses

Ref	Expression
ctiunct.som	⊢ (𝜑 → 𝑆 ⊆ ω)
ctiunct.sdc	⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)
ctiunct.f	⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)
ctiunct.tom	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)
ctiunct.tdc	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)
ctiunct.g	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)
ctiunct.j	⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))
ctiunct.u	⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}

Assertion

Ref	Expression
ctiunctlemuom	⊢ (𝜑 → 𝑈 ⊆ ω)

Proof of Theorem ctiunctlemuom

Step	Hyp	Ref	Expression
1		ctiunct.u	. . 3 ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}
2		ssrab2 3187	. . 3 ⊢ {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)} ⊆ ω
3	1, 2	eqsstri 3134	. 2 ⊢ 𝑈 ⊆ ω
4	3	a1i 9	1 ⊢ (𝜑 → 𝑈 ⊆ ω)

Syntax hints:   → wi 4   ∧ wa 103  DECID wdc 820   = wceq 1332   ∈ wcel 1481  ∀wral 2417  {crab 2421  ⦋csb 3007   ⊆ wss 3076  ωcom 4512   × cxp 4545  –onto→wfo 5129  –1-1-onto→wf1o 5130  ‘cfv 5131  1^st c1st 6044  2^nd c2nd 6045

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-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rab 2426  df-in 3082  df-ss 3089

This theorem is referenced by:  ctiunct  11989