Theorem ctiunct 12977

Description: A sequence of enumerations gives an enumeration of the union. We refer to "sequence of enumerations" rather than "countably many countable sets" because the hypothesis provides more than countability for each 𝐵(𝑥): it refers to 𝐵(𝑥) together with the 𝐺(𝑥) which enumerates it. Theorem 8.1.19 of [AczelRathjen], p. 74.

For "countably many countable sets" the key hypothesis would be (𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑔𝑔:ω–onto→(𝐵 ⊔ 1_o). This is almost omiunct 12981 (which uses countable choice) although that is for a countably infinite collection not any countable collection.

Compare with the case of two sets instead of countably many, as seen at unct 12979, which says that the union of two countable sets is countable .

The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 12932) and using the first number to map to an element 𝑥 of 𝐴 and the second number to map to an element of B(x) . In this way we are able to map to every element of ∪ 𝑥 ∈ 𝐴𝐵. Although it would be possible to work directly with countability expressed as 𝐹:ω–onto→(𝐴 ⊔ 1_o), we instead use functions from subsets of the natural numbers via ctssdccl 7246 and ctssdc 7248.

(Contributed by Jim Kingdon, 31-Oct-2023.)

Hypotheses

Ref	Expression
ctiunct.a	⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o))
ctiunct.b	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:ω–onto→(𝐵 ⊔ 1o))

Assertion

Ref	Expression
ctiunct	⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))

Distinct variable groups:   𝐴,ℎ,𝑥   𝐵,ℎ   𝑥,𝐹   𝜑,𝑥

Allowed substitution hints:   𝜑(ℎ)   𝐵(𝑥)   𝐹(ℎ)   𝐺(𝑥,ℎ)

Proof of Theorem ctiunct

Dummy variables 𝑗 𝑘 𝑛 𝑢 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpomen 12932	. . . . 5 ⊢ (ω × ω) ≈ ω
2	1	ensymi 6904	. . . 4 ⊢ ω ≈ (ω × ω)
3		bren 6865	. . . 4 ⊢ (ω ≈ (ω × ω) ↔ ∃𝑗 𝑗:ω–1-1-onto→(ω × ω))
4	2, 3	mpbi 145	. . 3 ⊢ ∃𝑗 𝑗:ω–1-1-onto→(ω × ω)
5	4	a1i 9	. 2 ⊢ (𝜑 → ∃𝑗 𝑗:ω–1-1-onto→(ω × ω))
6		ctiunct.a	. . . . . . . 8 ⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o))
7		eqid 2209	. . . . . . . 8 ⊢ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} = {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}
8		eqid 2209	. . . . . . . 8 ⊢ (◡inl ∘ 𝐹) = (◡inl ∘ 𝐹)
9	6, 7, 8	ctssdccl 7246	. . . . . . 7 ⊢ (𝜑 → ({𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ⊆ ω ∧ (◡inl ∘ 𝐹):{𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}))
10	9	simp1d 1014	. . . . . 6 ⊢ (𝜑 → {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ⊆ ω)
11	10	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ⊆ ω)
12	9	simp3d 1016	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)})
13	12	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)})
14	9	simp2d 1015	. . . . . 6 ⊢ (𝜑 → (◡inl ∘ 𝐹):{𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}–onto→𝐴)
15	14	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → (◡inl ∘ 𝐹):{𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}–onto→𝐴)
16		ctiunct.b	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:ω–onto→(𝐵 ⊔ 1o))
17		eqid 2209	. . . . . . . 8 ⊢ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} = {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}
18		eqid 2209	. . . . . . . 8 ⊢ (◡inl ∘ 𝐺) = (◡inl ∘ 𝐺)
19	16, 17, 18	ctssdccl 7246	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} ⊆ ω ∧ (◡inl ∘ 𝐺):{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}–onto→𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}))
20	19	simp1d 1014	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} ⊆ ω)
21	20	adantlr 477	. . . . 5 ⊢ (((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) ∧ 𝑥 ∈ 𝐴) → {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} ⊆ ω)
22	19	simp3d 1016	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})
23	22	adantlr 477	. . . . 5 ⊢ (((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})
24	19	simp2d 1015	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (◡inl ∘ 𝐺):{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}–onto→𝐵)
25	24	adantlr 477	. . . . 5 ⊢ (((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) ∧ 𝑥 ∈ 𝐴) → (◡inl ∘ 𝐺):{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}–onto→𝐵)
26		simpr 110	. . . . 5 ⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → 𝑗:ω–1-1-onto→(ω × ω))
27		eqid 2209	. . . . 5 ⊢ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} = {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}
28	11, 13, 15, 21, 23, 25, 26, 27	ctiunctlemuom 12973	. . . 4 ⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ⊆ ω)
29		eqid 2209	. . . . . 6 ⊢ (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) = (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛))))
30		nfv 1554	. . . . . . . . 9 ⊢ Ⅎ𝑥(1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}
31		nfcsb1v 3137	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}
32	31	nfel2 2365	. . . . . . . . 9 ⊢ Ⅎ𝑥(2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}
33	30, 32	nfan 1591	. . . . . . . 8 ⊢ Ⅎ𝑥((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})
34		nfcv 2352	. . . . . . . 8 ⊢ Ⅎ𝑥ω
35	33, 34	nfrabw 2692	. . . . . . 7 ⊢ Ⅎ𝑥{𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}
36		nfcsb1v 3137	. . . . . . . 8 ⊢ Ⅎ𝑥⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)
37		nfcv 2352	. . . . . . . 8 ⊢ Ⅎ𝑥(2nd ‘(𝑗‘𝑛))
38	36, 37	nffv 5613	. . . . . . 7 ⊢ Ⅎ𝑥(⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))
39	35, 38	nfmpt 4155	. . . . . 6 ⊢ Ⅎ𝑥(𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛))))
40	11, 13, 15, 21, 23, 25, 26, 27, 29, 39, 35	ctiunctlemfo 12976	. . . . 5 ⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))):{𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵)
41		omex 4662	. . . . . . . 8 ⊢ ω ∈ V
42	41	rabex 4207	. . . . . . 7 ⊢ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ∈ V
43	42	mptex 5838	. . . . . 6 ⊢ (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) ∈ V
44		foeq1 5520	. . . . . 6 ⊢ (𝑘 = (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) → (𝑘:{𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))):{𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵))
45	43, 44	spcev 2878	. . . . 5 ⊢ ((𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))):{𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑘 𝑘:{𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵)
46	40, 45	syl 14	. . . 4 ⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → ∃𝑘 𝑘:{𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵)
47	11, 13, 15, 21, 23, 25, 26, 27	ctiunctlemudc 12974	. . . 4 ⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})})
48		sseq1 3227	. . . . . 6 ⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (𝑢 ⊆ ω ↔ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ⊆ ω))
49		foeq2 5521	. . . . . . 7 ⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑘:{𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵))
50	49	exbidv 1851	. . . . . 6 ⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑘 𝑘:{𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵))
51		eleq2 2273	. . . . . . . 8 ⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (𝑛 ∈ 𝑢 ↔ 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}))
52	51	dcbid 842	. . . . . . 7 ⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (DECID 𝑛 ∈ 𝑢 ↔ DECID 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}))
53	52	ralbidv 2510	. . . . . 6 ⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢 ↔ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}))
54	48, 50, 53	3anbi123d 1327	. . . . 5 ⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → ((𝑢 ⊆ ω ∧ ∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢) ↔ ({𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ⊆ ω ∧ ∃𝑘 𝑘:{𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})})))
55	42, 54	spcev 2878	. . . 4 ⊢ (({𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ⊆ ω ∧ ∃𝑘 𝑘:{𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}) → ∃𝑢(𝑢 ⊆ ω ∧ ∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢))
56	28, 46, 47, 55	syl3anc 1252	. . 3 ⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → ∃𝑢(𝑢 ⊆ ω ∧ ∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢))
57		ctssdc 7248	. . . 4 ⊢ (∃𝑢(𝑢 ⊆ ω ∧ ∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢) ↔ ∃𝑘 𝑘:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))
58		foeq1 5520	. . . . 5 ⊢ (𝑘 = ℎ → (𝑘:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o) ↔ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o)))
59	58	cbvexv 1945	. . . 4 ⊢ (∃𝑘 𝑘:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o) ↔ ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))
60	57, 59	bitri 184	. . 3 ⊢ (∃𝑢(𝑢 ⊆ ω ∧ ∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢) ↔ ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))
61	56, 60	sylib 122	. 2 ⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))
62	5, 61	exlimddv 1925	1 ⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))

Syntax hints:   → wi 4   ∧ wa 104  DECID wdc 838   ∧ w3a 983   = wceq 1375  ∃wex 1518   ∈ wcel 2180  ∀wral 2488  {crab 2492  ⦋csb 3104   ⊆ wss 3177  ∪ ciun 3944   class class class wbr 4062   ↦ cmpt 4124  ωcom 4659   × cxp 4694  ^◡ccnv 4695   “ cima 4699   ∘ ccom 4700  –onto→wfo 5292  –1-1-onto→wf1o 5293  ‘cfv 5294  1^st c1st 6254  2^nd c2nd 6255  1_oc1o 6525   ≈ cen 6855   ⊔ cdju 7172  inlcinl 7180

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 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-coll 4178  ax-sep 4181  ax-nul 4189  ax-pow 4237  ax-pr 4272  ax-un 4501  ax-setind 4606  ax-iinf 4657  ax-cnex 8058  ax-resscn 8059  ax-1cn 8060  ax-1re 8061  ax-icn 8062  ax-addcl 8063  ax-addrcl 8064  ax-mulcl 8065  ax-mulrcl 8066  ax-addcom 8067  ax-mulcom 8068  ax-addass 8069  ax-mulass 8070  ax-distr 8071  ax-i2m1 8072  ax-0lt1 8073  ax-1rid 8074  ax-0id 8075  ax-rnegex 8076  ax-precex 8077  ax-cnre 8078  ax-pre-ltirr 8079  ax-pre-ltwlin 8080  ax-pre-lttrn 8081  ax-pre-apti 8082  ax-pre-ltadd 8083  ax-pre-mulgt0 8084  ax-pre-mulext 8085  ax-arch 8086

This theorem depends on definitions:  df-bi 117  df-dc 839  df-3or 984  df-3an 985  df-tru 1378  df-fal 1381  df-xor 1398  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-nel 2476  df-ral 2493  df-rex 2494  df-reu 2495  df-rmo 2496  df-rab 2497  df-v 2781  df-sbc 3009  df-csb 3105  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-nul 3472  df-if 3583  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-int 3903  df-iun 3946  df-br 4063  df-opab 4125  df-mpt 4126  df-tr 4162  df-id 4361  df-po 4364  df-iso 4365  df-iord 4434  df-on 4436  df-ilim 4437  df-suc 4439  df-iom 4660  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-iota 5254  df-fun 5296  df-fn 5297  df-f 5298  df-f1 5299  df-fo 5300  df-f1o 5301  df-fv 5302  df-riota 5927  df-ov 5977  df-oprab 5978  df-mpo 5979  df-1st 6256  df-2nd 6257  df-recs 6421  df-frec 6507  df-1o 6532  df-er 6650  df-en 6858  df-dju 7173  df-inl 7182  df-inr 7183  df-case 7219  df-pnf 8151  df-mnf 8152  df-xr 8153  df-ltxr 8154  df-le 8155  df-sub 8287  df-neg 8288  df-reap 8690  df-ap 8697  df-div 8788  df-inn 9079  df-2 9137  df-n0 9338  df-z 9415  df-uz 9691  df-q 9783  df-rp 9818  df-fz 10173  df-fl 10457  df-mod 10512  df-seqfrec 10637  df-exp 10728  df-dvds 12265

This theorem is referenced by:  ctiunctal  12978  unct  12979