Theorem ctiunctlemfo 12596

Description: Lemma for ctiunct 12597. (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 12595	. 2 ⊢ (𝜑 → 𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵)
11		nfv 1539	. . . . 5 ⊢ Ⅎ𝑥𝜑
12		nfiu1 3942	. . . . . 6 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
13	12	nfcri 2330	. . . . 5 ⊢ Ⅎ𝑥 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
14	11, 13	nfan 1576	. . . 4 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
15		ctiunct.nfu	. . . . 5 ⊢ Ⅎ𝑥𝑈
16		ctiunct.nfh	. . . . . . 7 ⊢ Ⅎ𝑥𝐻
17		nfcv 2336	. . . . . . 7 ⊢ Ⅎ𝑥𝑣
18	16, 17	nffv 5564	. . . . . 6 ⊢ Ⅎ𝑥(𝐻‘𝑣)
19	18	nfeq2 2348	. . . . 5 ⊢ Ⅎ𝑥 𝑢 = (𝐻‘𝑣)
20	15, 19	nfrexw 2533	. . . 4 ⊢ Ⅎ𝑥∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣)
21		simplll 533	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝜑)
22		simplr 528	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝑥 ∈ 𝐴)
23	21, 22, 6	syl2anc 411	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝐺:𝑇–onto→𝐵)
24		foelrn 5795	. . . . . 6 ⊢ ((𝐺:𝑇–onto→𝐵 ∧ 𝑢 ∈ 𝐵) → ∃𝑤 ∈ 𝑇 𝑢 = (𝐺‘𝑤))
25	23, 24	sylancom 420	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → ∃𝑤 ∈ 𝑇 𝑢 = (𝐺‘𝑤))
26	3	ad4antr 494	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → 𝐹:𝑆–onto→𝐴)
27		simpllr 534	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → 𝑥 ∈ 𝐴)
28		foelrn 5795	. . . . . . 7 ⊢ ((𝐹:𝑆–onto→𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑟 ∈ 𝑆 𝑥 = (𝐹‘𝑟))
29	26, 27, 28	syl2anc 411	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → ∃𝑟 ∈ 𝑆 𝑥 = (𝐹‘𝑟))
30		f1ocnv 5513	. . . . . . . . . . . 12 ⊢ (𝐽:ω–1-1-onto→(ω × ω) → ◡𝐽:(ω × ω)–1-1-onto→ω)
31	7, 30	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → ◡𝐽:(ω × ω)–1-1-onto→ω)
32		f1of 5500	. . . . . . . . . . 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 3180	. . . . . . . . . 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 3180	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑤 ∈ ω)
43	37, 42	opelxpd 4692	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⟨𝑟, 𝑤⟩ ∈ (ω × ω))
44	34, 43	ffvelcdmd 5694	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (◡𝐽‘⟨𝑟, 𝑤⟩) ∈ ω)
45	38, 7	syl 14	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝐽:ω–1-1-onto→(ω × ω))
46		f1ocnvfv2 5821	. . . . . . . . . . . . 13 ⊢ ((𝐽:ω–1-1-onto→(ω × ω) ∧ ⟨𝑟, 𝑤⟩ ∈ (ω × ω)) → (𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = ⟨𝑟, 𝑤⟩)
47	45, 43, 46	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = ⟨𝑟, 𝑤⟩)
48	47	fveq2d 5558	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = (1st ‘⟨𝑟, 𝑤⟩))
49		vex 2763	. . . . . . . . . . . 12 ⊢ 𝑟 ∈ V
50		vex 2763	. . . . . . . . . . . 12 ⊢ 𝑤 ∈ V
51	49, 50	op1st 6199	. . . . . . . . . . 11 ⊢ (1st ‘⟨𝑟, 𝑤⟩) = 𝑟
52	48, 51	eqtrdi 2242	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = 𝑟)
53	52, 36	eqeltrd 2270	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆)
54	47	fveq2d 5558	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = (2nd ‘⟨𝑟, 𝑤⟩))
55	49, 50	op2nd 6200	. . . . . . . . . . 11 ⊢ (2nd ‘⟨𝑟, 𝑤⟩) = 𝑤
56	54, 55	eqtrdi 2242	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = 𝑤)
57	52	fveq2d 5558	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = (𝐹‘𝑟))
58		simprr 531	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑥 = (𝐹‘𝑟))
59	57, 58	eqtr4d 2229	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = 𝑥)
60	59	csbeq1d 3087	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇 = ⦋𝑥 / 𝑥⦌𝑇)
61		csbid 3088	. . . . . . . . . . 11 ⊢ ⦋𝑥 / 𝑥⦌𝑇 = 𝑇
62	60, 61	eqtrdi 2242	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇 = 𝑇)
63	41, 56, 62	3eltr4d 2277	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)
64	53, 63	jca 306	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇))
65		2fveq3 5559	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (1st ‘(𝐽‘𝑧)) = (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
66	65	eleq1d 2262	. . . . . . . . . 10 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ↔ (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆))
67		2fveq3 5559	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (2nd ‘(𝐽‘𝑧)) = (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
68	65	fveq2d 5558	. . . . . . . . . . . 12 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐹‘(1st ‘(𝐽‘𝑧))) = (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
69	68	csbeq1d 3087	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇 = ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)
70	67, 69	eleq12d 2264	. . . . . . . . . 10 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ((2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇 ↔ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇))
71	66, 70	anbi12d 473	. . . . . . . . 9 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇) ↔ ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)))
72	71, 8	elrab2 2919	. . . . . . . 8 ⊢ ((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈 ↔ ((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ ω ∧ ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)))
73	44, 64, 72	sylanbrc 417	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈)
74	59	csbeq1d 3087	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺 = ⦋𝑥 / 𝑥⦌𝐺)
75		csbid 3088	. . . . . . . . . 10 ⊢ ⦋𝑥 / 𝑥⦌𝐺 = 𝐺
76	74, 75	eqtrdi 2242	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺 = 𝐺)
77	76, 56	fveq12d 5561	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = (𝐺‘𝑤))
78		2fveq3 5559	. . . . . . . . . . . 12 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (1st ‘(𝐽‘𝑛)) = (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
79	78	fveq2d 5558	. . . . . . . . . . 11 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐹‘(1st ‘(𝐽‘𝑛))) = (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
80	79	csbeq1d 3087	. . . . . . . . . 10 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺 = ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺)
81		2fveq3 5559	. . . . . . . . . 10 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (2nd ‘(𝐽‘𝑛)) = (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
82	80, 81	fveq12d 5561	. . . . . . . . 9 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛))) = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
83		simplrr 536	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (𝐺‘𝑤))
84	83, 77	eqtr4d 2229	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
85		simpllr 534	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 ∈ 𝐵)
86	84, 85	eqeltrrd 2271	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) ∈ 𝐵)
87	9, 82, 73, 86	fvmptd3 5651	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
88	77, 87, 83	3eqtr4rd 2237	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)))
89		fveq2 5554	. . . . . . . 8 ⊢ (𝑣 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐻‘𝑣) = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)))
90	89	rspceeqv 2882	. . . . . . 7 ⊢ (((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈 ∧ 𝑢 = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
91	73, 88, 90	syl2anc 411	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
92	29, 91	rexlimddv 2616	. . . . 5 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
93	25, 92	rexlimddv 2616	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
94		eliun 3916	. . . . . 6 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
95	94	biimpi 120	. . . . 5 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
96	95	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
97	14, 20, 93, 96	r19.29af2 2634	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
98	97	ralrimiva 2567	. 2 ⊢ (𝜑 → ∀𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
99		dffo3 5705	. 2 ⊢ (𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ (𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣)))
100	10, 98, 99	sylanbrc 417	1 ⊢ (𝜑 → 𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∧ wa 104  DECID wdc 835   = wceq 1364   ∈ wcel 2164  Ⅎwnfc 2323  ∀wral 2472  ∃wrex 2473  {crab 2476  ⦋csb 3080   ⊆ wss 3153  ⟨cop 3621  ∪ ciun 3912   ↦ cmpt 4090  ωcom 4622   × cxp 4657  ^◡ccnv 4658  ⟶wf 5250  –onto→wfo 5252  –1-1-onto→wf1o 5253  ‘cfv 5254  1^st c1st 6191  2^nd c2nd 6192

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 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 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-1st 6193  df-2nd 6194

This theorem is referenced by:  ctiunct  12597