Theorem ctiunctlemfo 12398

Description: Lemma for ctiunct 12399. (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 12397	. 2 ⊢ (𝜑 → 𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵)
11		nfv 1522	. . . . 5 ⊢ Ⅎ𝑥𝜑
12		nfiu1 3904	. . . . . 6 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
13	12	nfcri 2307	. . . . 5 ⊢ Ⅎ𝑥 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
14	11, 13	nfan 1559	. . . 4 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
15		ctiunct.nfu	. . . . 5 ⊢ Ⅎ𝑥𝑈
16		ctiunct.nfh	. . . . . . 7 ⊢ Ⅎ𝑥𝐻
17		nfcv 2313	. . . . . . 7 ⊢ Ⅎ𝑥𝑣
18	16, 17	nffv 5509	. . . . . 6 ⊢ Ⅎ𝑥(𝐻‘𝑣)
19	18	nfeq2 2325	. . . . 5 ⊢ Ⅎ𝑥 𝑢 = (𝐻‘𝑣)
20	15, 19	nfrexxy 2510	. . . 4 ⊢ Ⅎ𝑥∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣)
21		simplll 529	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝜑)
22		simplr 526	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝑥 ∈ 𝐴)
23	21, 22, 6	syl2anc 409	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝐺:𝑇–onto→𝐵)
24		foelrn 5736	. . . . . 6 ⊢ ((𝐺:𝑇–onto→𝐵 ∧ 𝑢 ∈ 𝐵) → ∃𝑤 ∈ 𝑇 𝑢 = (𝐺‘𝑤))
25	23, 24	sylancom 418	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → ∃𝑤 ∈ 𝑇 𝑢 = (𝐺‘𝑤))
26	3	ad4antr 492	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → 𝐹:𝑆–onto→𝐴)
27		simpllr 530	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → 𝑥 ∈ 𝐴)
28		foelrn 5736	. . . . . . 7 ⊢ ((𝐹:𝑆–onto→𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑟 ∈ 𝑆 𝑥 = (𝐹‘𝑟))
29	26, 27, 28	syl2anc 409	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → ∃𝑟 ∈ 𝑆 𝑥 = (𝐹‘𝑟))
30		f1ocnv 5458	. . . . . . . . . . . 12 ⊢ (𝐽:ω–1-1-onto→(ω × ω) → ◡𝐽:(ω × ω)–1-1-onto→ω)
31	7, 30	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → ◡𝐽:(ω × ω)–1-1-onto→ω)
32		f1of 5445	. . . . . . . . . . 11 ⊢ (◡𝐽:(ω × ω)–1-1-onto→ω → ◡𝐽:(ω × ω)⟶ω)
33	31, 32	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐽:(ω × ω)⟶ω)
34	33	ad5antr 494	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ◡𝐽:(ω × ω)⟶ω)
35	1	ad5antr 494	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑆 ⊆ ω)
36		simprl 527	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑟 ∈ 𝑆)
37	35, 36	sseldd 3149	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑟 ∈ ω)
38		simp-5l 539	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝜑)
39	27	adantr 274	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑥 ∈ 𝐴)
40	38, 39, 4	syl2anc 409	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑇 ⊆ ω)
41		simplrl 531	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑤 ∈ 𝑇)
42	40, 41	sseldd 3149	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑤 ∈ ω)
43	37, 42	opelxpd 4645	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⟨𝑟, 𝑤⟩ ∈ (ω × ω))
44	34, 43	ffvelrnd 5636	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (◡𝐽‘⟨𝑟, 𝑤⟩) ∈ ω)
45	38, 7	syl 14	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝐽:ω–1-1-onto→(ω × ω))
46		f1ocnvfv2 5761	. . . . . . . . . . . . 13 ⊢ ((𝐽:ω–1-1-onto→(ω × ω) ∧ ⟨𝑟, 𝑤⟩ ∈ (ω × ω)) → (𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = ⟨𝑟, 𝑤⟩)
47	45, 43, 46	syl2anc 409	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = ⟨𝑟, 𝑤⟩)
48	47	fveq2d 5503	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = (1st ‘⟨𝑟, 𝑤⟩))
49		vex 2734	. . . . . . . . . . . 12 ⊢ 𝑟 ∈ V
50		vex 2734	. . . . . . . . . . . 12 ⊢ 𝑤 ∈ V
51	49, 50	op1st 6129	. . . . . . . . . . 11 ⊢ (1st ‘⟨𝑟, 𝑤⟩) = 𝑟
52	48, 51	eqtrdi 2220	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = 𝑟)
53	52, 36	eqeltrd 2248	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆)
54	47	fveq2d 5503	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = (2nd ‘⟨𝑟, 𝑤⟩))
55	49, 50	op2nd 6130	. . . . . . . . . . 11 ⊢ (2nd ‘⟨𝑟, 𝑤⟩) = 𝑤
56	54, 55	eqtrdi 2220	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = 𝑤)
57	52	fveq2d 5503	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = (𝐹‘𝑟))
58		simprr 528	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑥 = (𝐹‘𝑟))
59	57, 58	eqtr4d 2207	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = 𝑥)
60	59	csbeq1d 3057	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇 = ⦋𝑥 / 𝑥⦌𝑇)
61		csbid 3058	. . . . . . . . . . 11 ⊢ ⦋𝑥 / 𝑥⦌𝑇 = 𝑇
62	60, 61	eqtrdi 2220	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇 = 𝑇)
63	41, 56, 62	3eltr4d 2255	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)
64	53, 63	jca 304	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇))
65		2fveq3 5504	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (1st ‘(𝐽‘𝑧)) = (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
66	65	eleq1d 2240	. . . . . . . . . 10 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ↔ (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆))
67		2fveq3 5504	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (2nd ‘(𝐽‘𝑧)) = (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
68	65	fveq2d 5503	. . . . . . . . . . . 12 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐹‘(1st ‘(𝐽‘𝑧))) = (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
69	68	csbeq1d 3057	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇 = ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)
70	67, 69	eleq12d 2242	. . . . . . . . . 10 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ((2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇 ↔ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇))
71	66, 70	anbi12d 471	. . . . . . . . 9 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇) ↔ ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)))
72	71, 8	elrab2 2890	. . . . . . . 8 ⊢ ((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈 ↔ ((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ ω ∧ ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)))
73	44, 64, 72	sylanbrc 415	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈)
74	59	csbeq1d 3057	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺 = ⦋𝑥 / 𝑥⦌𝐺)
75		csbid 3058	. . . . . . . . . 10 ⊢ ⦋𝑥 / 𝑥⦌𝐺 = 𝐺
76	74, 75	eqtrdi 2220	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺 = 𝐺)
77	76, 56	fveq12d 5506	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = (𝐺‘𝑤))
78		2fveq3 5504	. . . . . . . . . . . 12 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (1st ‘(𝐽‘𝑛)) = (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
79	78	fveq2d 5503	. . . . . . . . . . 11 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐹‘(1st ‘(𝐽‘𝑛))) = (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
80	79	csbeq1d 3057	. . . . . . . . . 10 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺 = ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺)
81		2fveq3 5504	. . . . . . . . . 10 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (2nd ‘(𝐽‘𝑛)) = (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
82	80, 81	fveq12d 5506	. . . . . . . . 9 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛))) = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
83		simplrr 532	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (𝐺‘𝑤))
84	83, 77	eqtr4d 2207	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
85		simpllr 530	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 ∈ 𝐵)
86	84, 85	eqeltrrd 2249	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) ∈ 𝐵)
87	9, 82, 73, 86	fvmptd3 5593	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
88	77, 87, 83	3eqtr4rd 2215	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)))
89		fveq2 5499	. . . . . . . 8 ⊢ (𝑣 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐻‘𝑣) = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)))
90	89	rspceeqv 2853	. . . . . . 7 ⊢ (((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈 ∧ 𝑢 = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
91	73, 88, 90	syl2anc 409	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
92	29, 91	rexlimddv 2593	. . . . 5 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
93	25, 92	rexlimddv 2593	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
94		eliun 3878	. . . . . 6 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
95	94	biimpi 119	. . . . 5 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
96	95	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
97	14, 20, 93, 96	r19.29af2 2611	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
98	97	ralrimiva 2544	. 2 ⊢ (𝜑 → ∀𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
99		dffo3 5647	. 2 ⊢ (𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ (𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣)))
100	10, 98, 99	sylanbrc 415	1 ⊢ (𝜑 → 𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∧ wa 103  DECID wdc 830   = wceq 1349   ∈ wcel 2142  Ⅎwnfc 2300  ∀wral 2449  ∃wrex 2450  {crab 2453  ⦋csb 3050   ⊆ wss 3122  ⟨cop 3587  ∪ ciun 3874   ↦ cmpt 4051  ωcom 4575   × cxp 4610  ^◡ccnv 4611  ⟶wf 5196  –onto→wfo 5198  –1-1-onto→wf1o 5199  ‘cfv 5200  1^st c1st 6121  2^nd c2nd 6122

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 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-pow 4161  ax-pr 4195  ax-un 4419

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-rab 2458  df-v 2733  df-sbc 2957  df-csb 3051  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-iun 3876  df-br 3991  df-opab 4052  df-mpt 4053  df-id 4279  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-res 4624  df-ima 4625  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-f1 5205  df-fo 5206  df-f1o 5207  df-fv 5208  df-1st 6123  df-2nd 6124

This theorem is referenced by:  ctiunct  12399