Theorem ctiunctlemfo 12423

Description: Lemma for ctiunct 12424. (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 12422	. 2 ⊢ (𝜑 → 𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵)
11		nfv 1528	. . . . 5 ⊢ Ⅎ𝑥𝜑
12		nfiu1 3914	. . . . . 6 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
13	12	nfcri 2313	. . . . 5 ⊢ Ⅎ𝑥 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
14	11, 13	nfan 1565	. . . 4 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
15		ctiunct.nfu	. . . . 5 ⊢ Ⅎ𝑥𝑈
16		ctiunct.nfh	. . . . . . 7 ⊢ Ⅎ𝑥𝐻
17		nfcv 2319	. . . . . . 7 ⊢ Ⅎ𝑥𝑣
18	16, 17	nffv 5521	. . . . . 6 ⊢ Ⅎ𝑥(𝐻‘𝑣)
19	18	nfeq2 2331	. . . . 5 ⊢ Ⅎ𝑥 𝑢 = (𝐻‘𝑣)
20	15, 19	nfrexxy 2516	. . . 4 ⊢ Ⅎ𝑥∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣)
21		simplll 533	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝜑)
22		simplr 528	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝑥 ∈ 𝐴)
23	21, 22, 6	syl2anc 411	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → 𝐺:𝑇–onto→𝐵)
24		foelrn 5748	. . . . . 6 ⊢ ((𝐺:𝑇–onto→𝐵 ∧ 𝑢 ∈ 𝐵) → ∃𝑤 ∈ 𝑇 𝑢 = (𝐺‘𝑤))
25	23, 24	sylancom 420	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → ∃𝑤 ∈ 𝑇 𝑢 = (𝐺‘𝑤))
26	3	ad4antr 494	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → 𝐹:𝑆–onto→𝐴)
27		simpllr 534	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → 𝑥 ∈ 𝐴)
28		foelrn 5748	. . . . . . 7 ⊢ ((𝐹:𝑆–onto→𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑟 ∈ 𝑆 𝑥 = (𝐹‘𝑟))
29	26, 27, 28	syl2anc 411	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → ∃𝑟 ∈ 𝑆 𝑥 = (𝐹‘𝑟))
30		f1ocnv 5470	. . . . . . . . . . . 12 ⊢ (𝐽:ω–1-1-onto→(ω × ω) → ◡𝐽:(ω × ω)–1-1-onto→ω)
31	7, 30	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → ◡𝐽:(ω × ω)–1-1-onto→ω)
32		f1of 5457	. . . . . . . . . . 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 3156	. . . . . . . . . 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 3156	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑤 ∈ ω)
43	37, 42	opelxpd 4656	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⟨𝑟, 𝑤⟩ ∈ (ω × ω))
44	34, 43	ffvelcdmd 5648	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (◡𝐽‘⟨𝑟, 𝑤⟩) ∈ ω)
45	38, 7	syl 14	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝐽:ω–1-1-onto→(ω × ω))
46		f1ocnvfv2 5773	. . . . . . . . . . . . 13 ⊢ ((𝐽:ω–1-1-onto→(ω × ω) ∧ ⟨𝑟, 𝑤⟩ ∈ (ω × ω)) → (𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = ⟨𝑟, 𝑤⟩)
47	45, 43, 46	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = ⟨𝑟, 𝑤⟩)
48	47	fveq2d 5515	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = (1st ‘⟨𝑟, 𝑤⟩))
49		vex 2740	. . . . . . . . . . . 12 ⊢ 𝑟 ∈ V
50		vex 2740	. . . . . . . . . . . 12 ⊢ 𝑤 ∈ V
51	49, 50	op1st 6141	. . . . . . . . . . 11 ⊢ (1st ‘⟨𝑟, 𝑤⟩) = 𝑟
52	48, 51	eqtrdi 2226	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = 𝑟)
53	52, 36	eqeltrd 2254	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆)
54	47	fveq2d 5515	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = (2nd ‘⟨𝑟, 𝑤⟩))
55	49, 50	op2nd 6142	. . . . . . . . . . 11 ⊢ (2nd ‘⟨𝑟, 𝑤⟩) = 𝑤
56	54, 55	eqtrdi 2226	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) = 𝑤)
57	52	fveq2d 5515	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = (𝐹‘𝑟))
58		simprr 531	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑥 = (𝐹‘𝑟))
59	57, 58	eqtr4d 2213	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = 𝑥)
60	59	csbeq1d 3064	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇 = ⦋𝑥 / 𝑥⦌𝑇)
61		csbid 3065	. . . . . . . . . . 11 ⊢ ⦋𝑥 / 𝑥⦌𝑇 = 𝑇
62	60, 61	eqtrdi 2226	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇 = 𝑇)
63	41, 56, 62	3eltr4d 2261	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)
64	53, 63	jca 306	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇))
65		2fveq3 5516	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (1st ‘(𝐽‘𝑧)) = (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
66	65	eleq1d 2246	. . . . . . . . . 10 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ↔ (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆))
67		2fveq3 5516	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (2nd ‘(𝐽‘𝑧)) = (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
68	65	fveq2d 5515	. . . . . . . . . . . 12 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐹‘(1st ‘(𝐽‘𝑧))) = (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
69	68	csbeq1d 3064	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇 = ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)
70	67, 69	eleq12d 2248	. . . . . . . . . 10 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ((2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇 ↔ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇))
71	66, 70	anbi12d 473	. . . . . . . . 9 ⊢ (𝑧 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇) ↔ ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)))
72	71, 8	elrab2 2896	. . . . . . . 8 ⊢ ((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈 ↔ ((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ ω ∧ ((1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ 𝑆 ∧ (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))) ∈ ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝑇)))
73	44, 64, 72	sylanbrc 417	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈)
74	59	csbeq1d 3064	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺 = ⦋𝑥 / 𝑥⦌𝐺)
75		csbid 3065	. . . . . . . . . 10 ⊢ ⦋𝑥 / 𝑥⦌𝐺 = 𝐺
76	74, 75	eqtrdi 2226	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺 = 𝐺)
77	76, 56	fveq12d 5518	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) = (𝐺‘𝑤))
78		2fveq3 5516	. . . . . . . . . . . 12 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (1st ‘(𝐽‘𝑛)) = (1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
79	78	fveq2d 5515	. . . . . . . . . . 11 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐹‘(1st ‘(𝐽‘𝑛))) = (𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
80	79	csbeq1d 3064	. . . . . . . . . 10 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → ⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺 = ⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺)
81		2fveq3 5516	. . . . . . . . . 10 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (2nd ‘(𝐽‘𝑛)) = (2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩))))
82	80, 81	fveq12d 5518	. . . . . . . . 9 ⊢ (𝑛 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛))) = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
83		simplrr 536	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (𝐺‘𝑤))
84	83, 77	eqtr4d 2213	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
85		simpllr 534	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 ∈ 𝐵)
86	84, 85	eqeltrrd 2255	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) ∈ 𝐵)
87	9, 82, 73, 86	fvmptd3 5605	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)) = (⦋(𝐹‘(1st ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘(◡𝐽‘⟨𝑟, 𝑤⟩)))))
88	77, 87, 83	3eqtr4rd 2221	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → 𝑢 = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)))
89		fveq2 5511	. . . . . . . 8 ⊢ (𝑣 = (◡𝐽‘⟨𝑟, 𝑤⟩) → (𝐻‘𝑣) = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩)))
90	89	rspceeqv 2859	. . . . . . 7 ⊢ (((◡𝐽‘⟨𝑟, 𝑤⟩) ∈ 𝑈 ∧ 𝑢 = (𝐻‘(◡𝐽‘⟨𝑟, 𝑤⟩))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
91	73, 88, 90	syl2anc 411	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) ∧ (𝑟 ∈ 𝑆 ∧ 𝑥 = (𝐹‘𝑟))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
92	29, 91	rexlimddv 2599	. . . . 5 ⊢ (((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) ∧ (𝑤 ∈ 𝑇 ∧ 𝑢 = (𝐺‘𝑤))) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
93	25, 92	rexlimddv 2599	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
94		eliun 3888	. . . . . 6 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
95	94	biimpi 120	. . . . 5 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
96	95	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐵)
97	14, 20, 93, 96	r19.29af2 2617	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
98	97	ralrimiva 2550	. 2 ⊢ (𝜑 → ∀𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣))
99		dffo3 5659	. 2 ⊢ (𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ (𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∃𝑣 ∈ 𝑈 𝑢 = (𝐻‘𝑣)))
100	10, 98, 99	sylanbrc 417	1 ⊢ (𝜑 → 𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∧ wa 104  DECID wdc 834   = wceq 1353   ∈ wcel 2148  Ⅎwnfc 2306  ∀wral 2455  ∃wrex 2456  {crab 2459  ⦋csb 3057   ⊆ wss 3129  ⟨cop 3594  ∪ ciun 3884   ↦ cmpt 4061  ωcom 4586   × cxp 4621  ^◡ccnv 4622  ⟶wf 5208  –onto→wfo 5210  –1-1-onto→wf1o 5211  ‘cfv 5212  1^st c1st 6133  2^nd c2nd 6134

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-1st 6135  df-2nd 6136

This theorem is referenced by:  ctiunct  12424