Theorem ptuncnv 22866

Description: Exhibit the converse function of the map 𝐺 which joins two product topologies on disjoint index sets. (Contributed by Mario Carneiro, 8-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)

Hypotheses

Ref	Expression
ptunhmeo.x	⊢ 𝑋 = ∪ 𝐾
ptunhmeo.y	⊢ 𝑌 = ∪ 𝐿
ptunhmeo.j	⊢ 𝐽 = (∏t‘𝐹)
ptunhmeo.k	⊢ 𝐾 = (∏t‘(𝐹 ↾ 𝐴))
ptunhmeo.l	⊢ 𝐿 = (∏t‘(𝐹 ↾ 𝐵))
ptunhmeo.g	⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥 ∪ 𝑦))
ptunhmeo.c	⊢ (𝜑 → 𝐶 ∈ 𝑉)
ptunhmeo.f	⊢ (𝜑 → 𝐹:𝐶⟶Top)
ptunhmeo.u	⊢ (𝜑 → 𝐶 = (𝐴 ∪ 𝐵))
ptunhmeo.i	⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)

Assertion

Ref	Expression
ptuncnv	⊢ (𝜑 → ◡𝐺 = (𝑧 ∈ ∪ 𝐽 ↦ ⟨(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)⟩))

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑧,𝐺   𝜑,𝑥,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝑥,𝐹,𝑦,𝑧   𝑥,𝐽,𝑦,𝑧   𝑥,𝐾,𝑦,𝑧   𝑥,𝐿,𝑦,𝑧   𝑧,𝑉   𝑥,𝑋,𝑦,𝑧   𝑥,𝑌,𝑦,𝑧

Allowed substitution hints:   𝐺(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem ptuncnv

Dummy variables 𝑘 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptunhmeo.g	. . . 4 ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥 ∪ 𝑦))
2		vex 3426	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3426	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	op1std 7814	. . . . . 6 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (1st ‘𝑤) = 𝑥)
5	2, 3	op2ndd 7815	. . . . . 6 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑤) = 𝑦)
6	4, 5	uneq12d 4094	. . . . 5 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) = (𝑥 ∪ 𝑦))
7	6	mpompt 7366	. . . 4 ⊢ (𝑤 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑤) ∪ (2nd ‘𝑤))) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥 ∪ 𝑦))
8	1, 7	eqtr4i 2769	. . 3 ⊢ 𝐺 = (𝑤 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
9		xp1st 7836	. . . . . . 7 ⊢ (𝑤 ∈ (𝑋 × 𝑌) → (1st ‘𝑤) ∈ 𝑋)
10	9	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → (1st ‘𝑤) ∈ 𝑋)
11		ixpeq2 8657	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ 𝐴 ∪ ((𝐹 ↾ 𝐴)‘𝑘) = ∪ (𝐹‘𝑘) → X𝑘 ∈ 𝐴 ∪ ((𝐹 ↾ 𝐴)‘𝑘) = X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘))
12		fvres 6775	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑘) = (𝐹‘𝑘))
13	12	unieqd 4850	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝐴 → ∪ ((𝐹 ↾ 𝐴)‘𝑘) = ∪ (𝐹‘𝑘))
14	11, 13	mprg 3077	. . . . . . . . 9 ⊢ X𝑘 ∈ 𝐴 ∪ ((𝐹 ↾ 𝐴)‘𝑘) = X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)
15		ptunhmeo.c	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
16		ssun1 4102	. . . . . . . . . . . 12 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
17		ptunhmeo.u	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 = (𝐴 ∪ 𝐵))
18	16, 17	sseqtrrid 3970	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
19	15, 18	ssexd 5243	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ V)
20		ptunhmeo.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐶⟶Top)
21	20, 18	fssresd 6625	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶Top)
22		ptunhmeo.k	. . . . . . . . . . 11 ⊢ 𝐾 = (∏t‘(𝐹 ↾ 𝐴))
23	22	ptuni 22653	. . . . . . . . . 10 ⊢ ((𝐴 ∈ V ∧ (𝐹 ↾ 𝐴):𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ ((𝐹 ↾ 𝐴)‘𝑘) = ∪ 𝐾)
24	19, 21, 23	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → X𝑘 ∈ 𝐴 ∪ ((𝐹 ↾ 𝐴)‘𝑘) = ∪ 𝐾)
25	14, 24	eqtr3id 2793	. . . . . . . 8 ⊢ (𝜑 → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ 𝐾)
26		ptunhmeo.x	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐾
27	25, 26	eqtr4di 2797	. . . . . . 7 ⊢ (𝜑 → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = 𝑋)
28	27	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = 𝑋)
29	10, 28	eleqtrrd 2842	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → (1st ‘𝑤) ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘))
30		xp2nd 7837	. . . . . . 7 ⊢ (𝑤 ∈ (𝑋 × 𝑌) → (2nd ‘𝑤) ∈ 𝑌)
31	30	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑤) ∈ 𝑌)
32	17	eqcomd 2744	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝐶)
33		ptunhmeo.i	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)
34		uneqdifeq 4420	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵))
35	18, 33, 34	syl2anc 583	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵))
36	32, 35	mpbid 231	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 ∖ 𝐴) = 𝐵)
37	36	ixpeq1d 8655	. . . . . . . 8 ⊢ (𝜑 → X𝑘 ∈ (𝐶 ∖ 𝐴)∪ (𝐹‘𝑘) = X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘))
38		ixpeq2 8657	. . . . . . . . . . 11 ⊢ (∀𝑘 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑘) = ∪ (𝐹‘𝑘) → X𝑘 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑘) = X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘))
39		fvres 6775	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑘) = (𝐹‘𝑘))
40	39	unieqd 4850	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝐵 → ∪ ((𝐹 ↾ 𝐵)‘𝑘) = ∪ (𝐹‘𝑘))
41	38, 40	mprg 3077	. . . . . . . . . 10 ⊢ X𝑘 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑘) = X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘)
42		ssun2 4103	. . . . . . . . . . . . 13 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
43	42, 17	sseqtrrid 3970	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
44	15, 43	ssexd 5243	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ V)
45	20, 43	fssresd 6625	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶Top)
46		ptunhmeo.l	. . . . . . . . . . . 12 ⊢ 𝐿 = (∏t‘(𝐹 ↾ 𝐵))
47	46	ptuni 22653	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top) → X𝑘 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑘) = ∪ 𝐿)
48	44, 45, 47	syl2anc 583	. . . . . . . . . 10 ⊢ (𝜑 → X𝑘 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑘) = ∪ 𝐿)
49	41, 48	eqtr3id 2793	. . . . . . . . 9 ⊢ (𝜑 → X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘) = ∪ 𝐿)
50		ptunhmeo.y	. . . . . . . . 9 ⊢ 𝑌 = ∪ 𝐿
51	49, 50	eqtr4di 2797	. . . . . . . 8 ⊢ (𝜑 → X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘) = 𝑌)
52	37, 51	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → X𝑘 ∈ (𝐶 ∖ 𝐴)∪ (𝐹‘𝑘) = 𝑌)
53	52	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → X𝑘 ∈ (𝐶 ∖ 𝐴)∪ (𝐹‘𝑘) = 𝑌)
54	31, 53	eleqtrrd 2842	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑤) ∈ X𝑘 ∈ (𝐶 ∖ 𝐴)∪ (𝐹‘𝑘))
55	18	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → 𝐴 ⊆ 𝐶)
56		undifixp 8680	. . . . 5 ⊢ (((1st ‘𝑤) ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∧ (2nd ‘𝑤) ∈ X𝑘 ∈ (𝐶 ∖ 𝐴)∪ (𝐹‘𝑘) ∧ 𝐴 ⊆ 𝐶) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ X𝑘 ∈ 𝐶 ∪ (𝐹‘𝑘))
57	29, 54, 55, 56	syl3anc 1369	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ X𝑘 ∈ 𝐶 ∪ (𝐹‘𝑘))
58		ptunhmeo.j	. . . . . . 7 ⊢ 𝐽 = (∏t‘𝐹)
59	58	ptuni 22653	. . . . . 6 ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐹:𝐶⟶Top) → X𝑘 ∈ 𝐶 ∪ (𝐹‘𝑘) = ∪ 𝐽)
60	15, 20, 59	syl2anc 583	. . . . 5 ⊢ (𝜑 → X𝑘 ∈ 𝐶 ∪ (𝐹‘𝑘) = ∪ 𝐽)
61	60	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → X𝑘 ∈ 𝐶 ∪ (𝐹‘𝑘) = ∪ 𝐽)
62	57, 61	eleqtrd 2841	. . 3 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ ∪ 𝐽)
63	18	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐽) → 𝐴 ⊆ 𝐶)
64	60	eleq2d 2824	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ X𝑘 ∈ 𝐶 ∪ (𝐹‘𝑘) ↔ 𝑧 ∈ ∪ 𝐽))
65	64	biimpar 477	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐽) → 𝑧 ∈ X𝑘 ∈ 𝐶 ∪ (𝐹‘𝑘))
66		resixp 8679	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝑧 ∈ X𝑘 ∈ 𝐶 ∪ (𝐹‘𝑘)) → (𝑧 ↾ 𝐴) ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘))
67	63, 65, 66	syl2anc 583	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐽) → (𝑧 ↾ 𝐴) ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘))
68	27	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐽) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = 𝑋)
69	67, 68	eleqtrd 2841	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐽) → (𝑧 ↾ 𝐴) ∈ 𝑋)
70	43	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐽) → 𝐵 ⊆ 𝐶)
71		resixp 8679	. . . . . 6 ⊢ ((𝐵 ⊆ 𝐶 ∧ 𝑧 ∈ X𝑘 ∈ 𝐶 ∪ (𝐹‘𝑘)) → (𝑧 ↾ 𝐵) ∈ X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘))
72	70, 65, 71	syl2anc 583	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐽) → (𝑧 ↾ 𝐵) ∈ X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘))
73	51	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐽) → X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘) = 𝑌)
74	72, 73	eleqtrd 2841	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐽) → (𝑧 ↾ 𝐵) ∈ 𝑌)
75	69, 74	opelxpd 5618	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐽) → ⟨(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)⟩ ∈ (𝑋 × 𝑌))
76		eqop 7846	. . . . 5 ⊢ (𝑤 ∈ (𝑋 × 𝑌) → (𝑤 = ⟨(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)⟩ ↔ ((1st ‘𝑤) = (𝑧 ↾ 𝐴) ∧ (2nd ‘𝑤) = (𝑧 ↾ 𝐵))))
77	76	ad2antrl 724	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (𝑤 = ⟨(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)⟩ ↔ ((1st ‘𝑤) = (𝑧 ↾ 𝐴) ∧ (2nd ‘𝑤) = (𝑧 ↾ 𝐵))))
78	65	adantrl 712	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → 𝑧 ∈ X𝑘 ∈ 𝐶 ∪ (𝐹‘𝑘))
79		ixpfn 8649	. . . . . . . . 9 ⊢ (𝑧 ∈ X𝑘 ∈ 𝐶 ∪ (𝐹‘𝑘) → 𝑧 Fn 𝐶)
80		fnresdm 6535	. . . . . . . . 9 ⊢ (𝑧 Fn 𝐶 → (𝑧 ↾ 𝐶) = 𝑧)
81	78, 79, 80	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (𝑧 ↾ 𝐶) = 𝑧)
82	17	reseq2d 5880	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ↾ 𝐶) = (𝑧 ↾ (𝐴 ∪ 𝐵)))
83	82	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (𝑧 ↾ 𝐶) = (𝑧 ↾ (𝐴 ∪ 𝐵)))
84	81, 83	eqtr3d 2780	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → 𝑧 = (𝑧 ↾ (𝐴 ∪ 𝐵)))
85		resundi 5894	. . . . . . 7 ⊢ (𝑧 ↾ (𝐴 ∪ 𝐵)) = ((𝑧 ↾ 𝐴) ∪ (𝑧 ↾ 𝐵))
86	84, 85	eqtrdi 2795	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → 𝑧 = ((𝑧 ↾ 𝐴) ∪ (𝑧 ↾ 𝐵)))
87		uneq12 4088	. . . . . . 7 ⊢ (((1st ‘𝑤) = (𝑧 ↾ 𝐴) ∧ (2nd ‘𝑤) = (𝑧 ↾ 𝐵)) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) = ((𝑧 ↾ 𝐴) ∪ (𝑧 ↾ 𝐵)))
88	87	eqeq2d 2749	. . . . . 6 ⊢ (((1st ‘𝑤) = (𝑧 ↾ 𝐴) ∧ (2nd ‘𝑤) = (𝑧 ↾ 𝐵)) → (𝑧 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↔ 𝑧 = ((𝑧 ↾ 𝐴) ∪ (𝑧 ↾ 𝐵))))
89	86, 88	syl5ibrcom 246	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (((1st ‘𝑤) = (𝑧 ↾ 𝐴) ∧ (2nd ‘𝑤) = (𝑧 ↾ 𝐵)) → 𝑧 = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
90		ixpfn 8649	. . . . . . . . . . . 12 ⊢ ((1st ‘𝑤) ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) → (1st ‘𝑤) Fn 𝐴)
91	29, 90	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → (1st ‘𝑤) Fn 𝐴)
92	91	adantrr 713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (1st ‘𝑤) Fn 𝐴)
93		dffn2 6586	. . . . . . . . . 10 ⊢ ((1st ‘𝑤) Fn 𝐴 ↔ (1st ‘𝑤):𝐴⟶V)
94	92, 93	sylib 217	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (1st ‘𝑤):𝐴⟶V)
95	51	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘) = 𝑌)
96	31, 95	eleqtrrd 2842	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑤) ∈ X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘))
97		ixpfn 8649	. . . . . . . . . . . 12 ⊢ ((2nd ‘𝑤) ∈ X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘) → (2nd ‘𝑤) Fn 𝐵)
98	96, 97	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑤) Fn 𝐵)
99	98	adantrr 713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (2nd ‘𝑤) Fn 𝐵)
100		dffn2 6586	. . . . . . . . . 10 ⊢ ((2nd ‘𝑤) Fn 𝐵 ↔ (2nd ‘𝑤):𝐵⟶V)
101	99, 100	sylib 217	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (2nd ‘𝑤):𝐵⟶V)
102		res0 5884	. . . . . . . . . . 11 ⊢ ((1st ‘𝑤) ↾ ∅) = ∅
103		res0 5884	. . . . . . . . . . 11 ⊢ ((2nd ‘𝑤) ↾ ∅) = ∅
104	102, 103	eqtr4i 2769	. . . . . . . . . 10 ⊢ ((1st ‘𝑤) ↾ ∅) = ((2nd ‘𝑤) ↾ ∅)
105	33	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (𝐴 ∩ 𝐵) = ∅)
106	105	reseq2d 5880	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → ((1st ‘𝑤) ↾ (𝐴 ∩ 𝐵)) = ((1st ‘𝑤) ↾ ∅))
107	105	reseq2d 5880	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → ((2nd ‘𝑤) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑤) ↾ ∅))
108	104, 106, 107	3eqtr4a 2805	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → ((1st ‘𝑤) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑤) ↾ (𝐴 ∩ 𝐵)))
109		fresaunres1 6631	. . . . . . . . 9 ⊢ (((1st ‘𝑤):𝐴⟶V ∧ (2nd ‘𝑤):𝐵⟶V ∧ ((1st ‘𝑤) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑤) ↾ (𝐴 ∩ 𝐵))) → (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐴) = (1st ‘𝑤))
110	94, 101, 108, 109	syl3anc 1369	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐴) = (1st ‘𝑤))
111	110	eqcomd 2744	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (1st ‘𝑤) = (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐴))
112		fresaunres2 6630	. . . . . . . . 9 ⊢ (((1st ‘𝑤):𝐴⟶V ∧ (2nd ‘𝑤):𝐵⟶V ∧ ((1st ‘𝑤) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑤) ↾ (𝐴 ∩ 𝐵))) → (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐵) = (2nd ‘𝑤))
113	94, 101, 108, 112	syl3anc 1369	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐵) = (2nd ‘𝑤))
114	113	eqcomd 2744	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (2nd ‘𝑤) = (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐵))
115	111, 114	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → ((1st ‘𝑤) = (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐴) ∧ (2nd ‘𝑤) = (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐵)))
116		reseq1 5874	. . . . . . . 8 ⊢ (𝑧 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) → (𝑧 ↾ 𝐴) = (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐴))
117	116	eqeq2d 2749	. . . . . . 7 ⊢ (𝑧 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) → ((1st ‘𝑤) = (𝑧 ↾ 𝐴) ↔ (1st ‘𝑤) = (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐴)))
118		reseq1 5874	. . . . . . . 8 ⊢ (𝑧 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) → (𝑧 ↾ 𝐵) = (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐵))
119	118	eqeq2d 2749	. . . . . . 7 ⊢ (𝑧 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) → ((2nd ‘𝑤) = (𝑧 ↾ 𝐵) ↔ (2nd ‘𝑤) = (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐵)))
120	117, 119	anbi12d 630	. . . . . 6 ⊢ (𝑧 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) → (((1st ‘𝑤) = (𝑧 ↾ 𝐴) ∧ (2nd ‘𝑤) = (𝑧 ↾ 𝐵)) ↔ ((1st ‘𝑤) = (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐴) ∧ (2nd ‘𝑤) = (((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↾ 𝐵))))
121	115, 120	syl5ibrcom 246	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (𝑧 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) → ((1st ‘𝑤) = (𝑧 ↾ 𝐴) ∧ (2nd ‘𝑤) = (𝑧 ↾ 𝐵))))
122	89, 121	impbid 211	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (((1st ‘𝑤) = (𝑧 ↾ 𝐴) ∧ (2nd ‘𝑤) = (𝑧 ↾ 𝐵)) ↔ 𝑧 = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
123	77, 122	bitrd 278	. . 3 ⊢ ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝐽)) → (𝑤 = ⟨(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)⟩ ↔ 𝑧 = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
124	8, 62, 75, 123	f1ocnv2d 7500	. 2 ⊢ (𝜑 → (𝐺:(𝑋 × 𝑌)–1-1-onto→∪ 𝐽 ∧ ◡𝐺 = (𝑧 ∈ ∪ 𝐽 ↦ ⟨(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)⟩)))
125	124	simprd 495	1 ⊢ (𝜑 → ◡𝐺 = (𝑧 ∈ ∪ 𝐽 ↦ ⟨(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)⟩))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  ⟨cop 4564  ∪ cuni 4836   ↦ cmpt 5153   × cxp 5578  ^◡ccnv 5579   ↾ cres 5582   Fn wfn 6413  ⟶wf 6414  –1-1-onto→wf1o 6417  ‘cfv 6418   ∈ cmpo 7257  1^st c1st 7802  2^nd c2nd 7803  Xcixp 8643  ∏_tcpt 17066  Topctop 21950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-1o 8267  df-er 8456  df-ixp 8644  df-en 8692  df-fin 8695  df-fi 9100  df-topgen 17071  df-pt 17072  df-top 21951  df-bases 22004

This theorem is referenced by:  ptunhmeo  22867