Theorem ctiunctlemfo 12681

Description: Lemma for ctiunct 12682. (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 ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}
ctiunct.h	⊢ 𝐻 = (𝑛 ∈ 𝑈 ↦ (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛))))
ctiunct.nfh	⊢ Ⅎ𝑥𝐻
ctiunct.nfu	⊢ Ⅎ𝑥𝑈

Assertion

Ref	Expression
ctiunctlemfo	⊢ (𝜑 → 𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵)

Distinct variable groups:   𝐴,𝑛,𝑥   𝐵,𝑛   𝑛,𝐹,𝑥,𝑧   𝑛,𝐺   𝑛,𝐽,𝑥,𝑧   𝑧,𝑆   𝑧,𝑇   𝑈,𝑛   𝜑,𝑛,𝑥   𝑧,𝑛

Allowed substitution hints:   𝜑(𝑧)   𝐴(𝑧)   𝐵(𝑥,𝑧)   𝑆(𝑥,𝑛)   𝑇(𝑥,𝑛)   𝑈(𝑥,𝑧)   𝐺(𝑥,𝑧)   𝐻(𝑥,𝑧,𝑛)

Proof of Theorem ctiunctlemfo

Dummy variables 𝑟 𝑤 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ctiunct.som	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ω)
2		ctiunct.sdc	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)
3		ctiunct.f	. . 3 ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)
4		ctiunct.tom	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)
5		ctiunct.tdc	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)
6		ctiunct.g	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)
7		ctiunct.j	. . 3 ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))
8		ctiunct.u	. . 3 ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}
9		ctiunct.h	. . 3 ⊢ 𝐻 = (𝑛 ∈ 𝑈 ↦ (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛))))
10	1, 2, 3, 4, 5, 6, 7, 8, 9	ctiunctlemf 12680	. 2 ⊢ (𝜑 → 𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵)
11		nfv 1542	. . . . 5 ⊢ Ⅎ𝑥𝜑
12		nfiu1 3947	. . . . . 6 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
13	12	nfcri 2333	. . . . 5 ⊢ Ⅎ𝑥 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
14	11, 13	nfan 1579	. . . 4 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
15		ctiunct.nfu	. . . . 5 ⊢ Ⅎ𝑥𝑈
16		ctiunct.nfh	. . . . . . 7 ⊢ Ⅎ𝑥𝐻
17		nfcv 2339	. . . . . . 7 ⊢ Ⅎ𝑥𝑣
18	16, 17	nffv 5571	. . . . . 6 ⊢ Ⅎ𝑥(𝐻‘𝑣)
19	18	nfeq2 2351	. . . . 5 ⊢ Ⅎ𝑥 𝑢 = (𝐻‘𝑣)
20	15, 19	nfrexw 2536	. . . 4 ⊢ Ⅎ𝑥∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣)
21		simplll 533	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝜑)
22		simplr 528	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝑥 ∈ 𝐴)
23	21, 22, 6	syl2anc 411	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝐺:𝑇–onto→𝐵)
24		foelrn 5802	. . . . . 6 ⊢ ((𝐺:𝑇–onto→𝐵 ∧ 𝑢 ∈ 𝐵) → ∃𝑤 ∈ 𝑇 𝑢 = (𝐺‘𝑤))
25	23, 24	sylancom 420	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → ∃𝑤 ∈ 𝑇 𝑢 = (𝐺‘𝑤))
26	3	ad4antr 494	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → 𝐹:𝑆–onto→𝐴)
27		simpllr 534	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → 𝑥 ∈ 𝐴)
28		foelrn 5802	. . . . . . 7 ⊢ ((𝐹:𝑆–onto→𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑟 ∈ 𝑆 𝑥 = (𝐹‘𝑟))
29	26, 27, 28	syl2anc 411	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → ∃𝑟 ∈ 𝑆 𝑥 = (𝐹‘𝑟))
30		f1ocnv 5520	. . . . . . . . . . . 12 ⊢ (𝐽:ω–1-1-onto→(ω × ω) → ◡𝐽:(ω × ω)–1-1-onto→ω)
31	7, 30	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → ◡𝐽:(ω × ω)–1-1-onto→ω)
32		f1of 5507	. . . . . . . . . . 11 ⊢ (◡𝐽:(ω × ω)–1-1-onto→ω → ◡𝐽:(ω × ω)⟶ω)
33	31, 32	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐽:(ω × ω)⟶ω)
34	33	ad5antr 496	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ◡𝐽:(ω × ω)⟶ω)
35	1	ad5antr 496	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑆 ⊆ ω)
36		simprl 529	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑟 ∈ 𝑆)
37	35, 36	sseldd 3185	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑟 ∈ ω)
38		simp-5l 543	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝜑)
39	27	adantr 276	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑥 ∈ 𝐴)
40	38, 39, 4	syl2anc 411	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑇 ⊆ ω)
41		simplrl 535	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑤 ∈ 𝑇)
42	40, 41	sseldd 3185	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑤 ∈ ω)
43	37, 42	opelxpd 4697	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⟨𝑟, 𝑤⟩ ∈ (ω × ω))
44	34, 43	ffvelcdmd 5701	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (◡𝐽‘⟨𝑟, 𝑤⟩) ∈ ω)
45	38, 7	syl 14	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝐽:ω–1-1-onto→(ω × ω))
46		f1ocnvfv2 5828	. . . . . . . . . . . . 13 ⊢ ((𝐽:ω–1-1-onto→(ω × ω) ∧ ⟨𝑟, 𝑤⟩ ∈ (ω × ω)) → (𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = ⟨𝑟, 𝑤⟩)
47	45, 43, 46	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = ⟨𝑟, 𝑤⟩)
48	47	fveq2d 5565	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = (1st ‘⟨𝑟, 𝑤⟩))
49		vex 2766	. . . . . . . . . . . 12 ⊢ 𝑟 ∈ V
50		vex 2766	. . . . . . . . . . . 12 ⊢ 𝑤 ∈ V
51	49, 50	op1st 6213	. . . . . . . . . . 11 ⊢ (1st ‘⟨𝑟, 𝑤⟩) = 𝑟
52	48, 51	eqtrdi 2245	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = 𝑟)
53	52, 36	eqeltrd 2273	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆)
54	47	fveq2d 5565	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = (2nd ‘⟨𝑟, 𝑤⟩))
55	49, 50	op2nd 6214	. . . . . . . . . . 11 ⊢ (2nd ‘⟨𝑟, 𝑤⟩) = 𝑤
56	54, 55	eqtrdi 2245	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = 𝑤)
57	52	fveq2d 5565	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = (𝐹‘𝑟))
58		simprr 531	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑥 = (𝐹‘𝑟))
59	57, 58	eqtr4d 2232	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = 𝑥)
60	59	csbeq1d 3091	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇 = ⦋𝑥 / 𝑥⦌𝑇)
61		csbid 3092	. . . . . . . . . . 11 ⊢ ⦋𝑥 / 𝑥⦌𝑇 = 𝑇
62	60, 61	eqtrdi 2245	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇 = 𝑇)
63	41, 56, 62	3eltr4d 2280	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)
64	53, 63	jca 306	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇))
65		2fveq3 5566	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (1st ‘(𝐽‘𝑧)) = (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
66	65	eleq1d 2265	. . . . . . . . . 10 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ↔ (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆))
67		2fveq3 5566	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (2nd ‘(𝐽‘𝑧)) = (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
68	65	fveq2d 5565	. . . . . . . . . . . 12 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐹‘(1st ‘(𝐽‘𝑧))) = (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
69	68	csbeq1d 3091	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇 = ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)
70	67, 69	eleq12d 2267	. . . . . . . . . 10 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ((2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇 ↔ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇))
71	66, 70	anbi12d 473	. . . . . . . . 9 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇) ↔ ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)))
72	71, 8	elrab2 2923	. . . . . . . 8 ⊢ ((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈 ↔ ((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ ω ∧ ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)))
73	44, 64, 72	sylanbrc 417	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈)
74	59	csbeq1d 3091	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺 = ⦋𝑥 / 𝑥⦌𝐺)
75		csbid 3092	. . . . . . . . . 10 ⊢ ⦋𝑥 / 𝑥⦌𝐺 = 𝐺
76	74, 75	eqtrdi 2245	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺 = 𝐺)
77	76, 56	fveq12d 5568	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = (𝐺‘𝑤))
78		2fveq3 5566	. . . . . . . . . . . 12 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (1st ‘(𝐽‘𝑛)) = (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
79	78	fveq2d 5565	. . . . . . . . . . 11 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐹‘(1st ‘(𝐽‘𝑛))) = (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
80	79	csbeq1d 3091	. . . . . . . . . 10 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺 = ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺)
81		2fveq3 5566	. . . . . . . . . 10 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (2nd ‘(𝐽‘𝑛)) = (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
82	80, 81	fveq12d 5568	. . . . . . . . 9 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛))) = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
83		simplrr 536	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (𝐺‘𝑤))
84	83, 77	eqtr4d 2232	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
85		simpllr 534	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 ∈ 𝐵)
86	84, 85	eqeltrrd 2274	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) ∈ 𝐵)
87	9, 82, 73, 86	fvmptd3 5658	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
88	77, 87, 83	3eqtr4rd 2240	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)))
89		fveq2 5561	. . . . . . . 8 ⊢ (𝑣 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐻‘𝑣) = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)))
90	89	rspceeqv 2886	. . . . . . 7 ⊢ (((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈 ∧ 𝑢 = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
91	73, 88, 90	syl2anc 411	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
92	29, 91	rexlimddv 2619	. . . . 5 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
93	25, 92	rexlimddv 2619	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
94		eliun 3921	. . . . . 6 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
95	94	biimpi 120	. . . . 5 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
96	95	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
97	14, 20, 93, 96	r19.29af2 2637	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
98	97	ralrimiva 2570	. 2 ⊢ (𝜑 → ∀𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
99		dffo3 5712	. 2 ⊢ (𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ (𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣)))
100	10, 98, 99	sylanbrc 417	1 ⊢ (𝜑 → 𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∧ wa 104  DECID wdc 835   = wceq 1364   ∈ wcel 2167  Ⅎwnfc 2326  ∀wral 2475  ∃wrex 2476  {crab 2479  ⦋csb 3084   ⊆ wss 3157  ⟨cop 3626  ∪ ciun 3917   ↦ cmpt 4095  ωcom 4627   × cxp 4662  ^◡ccnv 4663  ⟶wf 5255  –onto→wfo 5257  –1-1-onto→wf1o 5258  ‘cfv 5259  1^st c1st 6205  2^nd c2nd 6206

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-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243  ax-un 4469

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-iun 3919  df-br 4035  df-opab 4096  df-mpt 4097  df-id 4329  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-f1 5264  df-fo 5265  df-f1o 5266  df-fv 5267  df-1st 6207  df-2nd 6208

This theorem is referenced by:  ctiunct  12682