Theorem ctiunctlemfo 12372

Description: Lemma for ctiunct 12373. (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 12371	. 2 ⊢ (𝜑 → 𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵)
11		nfv 1516	. . . . 5 ⊢ Ⅎ𝑥𝜑
12		nfiu1 3896	. . . . . 6 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
13	12	nfcri 2302	. . . . 5 ⊢ Ⅎ𝑥 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
14	11, 13	nfan 1553	. . . 4 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
15		ctiunct.nfu	. . . . 5 ⊢ Ⅎ𝑥𝑈
16		ctiunct.nfh	. . . . . . 7 ⊢ Ⅎ𝑥𝐻
17		nfcv 2308	. . . . . . 7 ⊢ Ⅎ𝑥𝑣
18	16, 17	nffv 5496	. . . . . 6 ⊢ Ⅎ𝑥(𝐻‘𝑣)
19	18	nfeq2 2320	. . . . 5 ⊢ Ⅎ𝑥 𝑢 = (𝐻‘𝑣)
20	15, 19	nfrexxy 2505	. . . 4 ⊢ Ⅎ𝑥∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣)
21		simplll 523	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝜑)
22		simplr 520	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝑥 ∈ 𝐴)
23	21, 22, 6	syl2anc 409	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝐺:𝑇–onto→𝐵)
24		foelrn 5721	. . . . . 6 ⊢ ((𝐺:𝑇–onto→𝐵 ∧ 𝑢 ∈ 𝐵) → ∃𝑤 ∈ 𝑇 𝑢 = (𝐺‘𝑤))
25	23, 24	sylancom 417	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → ∃𝑤 ∈ 𝑇 𝑢 = (𝐺‘𝑤))
26	3	ad4antr 486	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → 𝐹:𝑆–onto→𝐴)
27		simpllr 524	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → 𝑥 ∈ 𝐴)
28		foelrn 5721	. . . . . . 7 ⊢ ((𝐹:𝑆–onto→𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑟 ∈ 𝑆 𝑥 = (𝐹‘𝑟))
29	26, 27, 28	syl2anc 409	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → ∃𝑟 ∈ 𝑆 𝑥 = (𝐹‘𝑟))
30		f1ocnv 5445	. . . . . . . . . . . 12 ⊢ (𝐽:ω–1-1-onto→(ω × ω) → ◡𝐽:(ω × ω)–1-1-onto→ω)
31	7, 30	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → ◡𝐽:(ω × ω)–1-1-onto→ω)
32		f1of 5432	. . . . . . . . . . 11 ⊢ (◡𝐽:(ω × ω)–1-1-onto→ω → ◡𝐽:(ω × ω)⟶ω)
33	31, 32	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐽:(ω × ω)⟶ω)
34	33	ad5antr 488	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ◡𝐽:(ω × ω)⟶ω)
35	1	ad5antr 488	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑆 ⊆ ω)
36		simprl 521	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑟 ∈ 𝑆)
37	35, 36	sseldd 3143	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑟 ∈ ω)
38		simp-5l 533	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝜑)
39	27	adantr 274	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑥 ∈ 𝐴)
40	38, 39, 4	syl2anc 409	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑇 ⊆ ω)
41		simplrl 525	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑤 ∈ 𝑇)
42	40, 41	sseldd 3143	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑤 ∈ ω)
43	37, 42	opelxpd 4637	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⟨𝑟, 𝑤⟩ ∈ (ω × ω))
44	34, 43	ffvelrnd 5621	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (◡𝐽‘⟨𝑟, 𝑤⟩) ∈ ω)
45	38, 7	syl 14	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝐽:ω–1-1-onto→(ω × ω))
46		f1ocnvfv2 5746	. . . . . . . . . . . . 13 ⊢ ((𝐽:ω–1-1-onto→(ω × ω) ∧ ⟨𝑟, 𝑤⟩ ∈ (ω × ω)) → (𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = ⟨𝑟, 𝑤⟩)
47	45, 43, 46	syl2anc 409	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = ⟨𝑟, 𝑤⟩)
48	47	fveq2d 5490	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = (1st ‘⟨𝑟, 𝑤⟩))
49		vex 2729	. . . . . . . . . . . 12 ⊢ 𝑟 ∈ V
50		vex 2729	. . . . . . . . . . . 12 ⊢ 𝑤 ∈ V
51	49, 50	op1st 6114	. . . . . . . . . . 11 ⊢ (1st ‘⟨𝑟, 𝑤⟩) = 𝑟
52	48, 51	eqtrdi 2215	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = 𝑟)
53	52, 36	eqeltrd 2243	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆)
54	47	fveq2d 5490	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = (2nd ‘⟨𝑟, 𝑤⟩))
55	49, 50	op2nd 6115	. . . . . . . . . . 11 ⊢ (2nd ‘⟨𝑟, 𝑤⟩) = 𝑤
56	54, 55	eqtrdi 2215	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = 𝑤)
57	52	fveq2d 5490	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = (𝐹‘𝑟))
58		simprr 522	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑥 = (𝐹‘𝑟))
59	57, 58	eqtr4d 2201	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = 𝑥)
60	59	csbeq1d 3052	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇 = ⦋𝑥 / 𝑥⦌𝑇)
61		csbid 3053	. . . . . . . . . . 11 ⊢ ⦋𝑥 / 𝑥⦌𝑇 = 𝑇
62	60, 61	eqtrdi 2215	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇 = 𝑇)
63	41, 56, 62	3eltr4d 2250	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)
64	53, 63	jca 304	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇))
65		2fveq3 5491	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (1st ‘(𝐽‘𝑧)) = (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
66	65	eleq1d 2235	. . . . . . . . . 10 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ↔ (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆))
67		2fveq3 5491	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (2nd ‘(𝐽‘𝑧)) = (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
68	65	fveq2d 5490	. . . . . . . . . . . 12 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐹‘(1st ‘(𝐽‘𝑧))) = (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
69	68	csbeq1d 3052	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇 = ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)
70	67, 69	eleq12d 2237	. . . . . . . . . 10 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ((2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇 ↔ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇))
71	66, 70	anbi12d 465	. . . . . . . . 9 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇) ↔ ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)))
72	71, 8	elrab2 2885	. . . . . . . 8 ⊢ ((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈 ↔ ((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ ω ∧ ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)))
73	44, 64, 72	sylanbrc 414	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈)
74	59	csbeq1d 3052	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺 = ⦋𝑥 / 𝑥⦌𝐺)
75		csbid 3053	. . . . . . . . . 10 ⊢ ⦋𝑥 / 𝑥⦌𝐺 = 𝐺
76	74, 75	eqtrdi 2215	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺 = 𝐺)
77	76, 56	fveq12d 5493	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = (𝐺‘𝑤))
78		2fveq3 5491	. . . . . . . . . . . 12 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (1st ‘(𝐽‘𝑛)) = (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
79	78	fveq2d 5490	. . . . . . . . . . 11 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐹‘(1st ‘(𝐽‘𝑛))) = (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
80	79	csbeq1d 3052	. . . . . . . . . 10 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺 = ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺)
81		2fveq3 5491	. . . . . . . . . 10 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (2nd ‘(𝐽‘𝑛)) = (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
82	80, 81	fveq12d 5493	. . . . . . . . 9 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛))) = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
83		simplrr 526	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (𝐺‘𝑤))
84	83, 77	eqtr4d 2201	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
85		simpllr 524	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 ∈ 𝐵)
86	84, 85	eqeltrrd 2244	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) ∈ 𝐵)
87	9, 82, 73, 86	fvmptd3 5579	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
88	77, 87, 83	3eqtr4rd 2209	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)))
89		fveq2 5486	. . . . . . . 8 ⊢ (𝑣 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐻‘𝑣) = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)))
90	89	rspceeqv 2848	. . . . . . 7 ⊢ (((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈 ∧ 𝑢 = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
91	73, 88, 90	syl2anc 409	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
92	29, 91	rexlimddv 2588	. . . . 5 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
93	25, 92	rexlimddv 2588	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
94		eliun 3870	. . . . . 6 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
95	94	biimpi 119	. . . . 5 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
96	95	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
97	14, 20, 93, 96	r19.29af2 2606	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
98	97	ralrimiva 2539	. 2 ⊢ (𝜑 → ∀𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
99		dffo3 5632	. 2 ⊢ (𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ (𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣)))
100	10, 98, 99	sylanbrc 414	1 ⊢ (𝜑 → 𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∧ wa 103  DECID wdc 824   = wceq 1343   ∈ wcel 2136  Ⅎwnfc 2295  ∀wral 2444  ∃wrex 2445  {crab 2448  ⦋csb 3045   ⊆ wss 3116  ⟨cop 3579  ∪ ciun 3866   ↦ cmpt 4043  ωcom 4567   × cxp 4602  ^◡ccnv 4603  ⟶wf 5184  –onto→wfo 5186  –1-1-onto→wf1o 5187  ‘cfv 5188  1^st c1st 6106  2^nd c2nd 6107

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-sep 4100  ax-pow 4153  ax-pr 4187  ax-un 4411

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-rex 2450  df-rab 2453  df-v 2728  df-sbc 2952  df-csb 3046  df-un 3120  df-in 3122  df-ss 3129  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-iun 3868  df-br 3983  df-opab 4044  df-mpt 4045  df-id 4271  df-xp 4610  df-rel 4611  df-cnv 4612  df-co 4613  df-dm 4614  df-rn 4615  df-res 4616  df-ima 4617  df-iota 5153  df-fun 5190  df-fn 5191  df-f 5192  df-f1 5193  df-fo 5194  df-f1o 5195  df-fv 5196  df-1st 6108  df-2nd 6109

This theorem is referenced by:  ctiunct  12373