ptuncnv

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

	Ref	Expression
Hypotheses	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	ptuncnv	⊢ ( 𝜑 → ^◡ 𝐺 = ( 𝑧 ∈ ∪ 𝐽 ↦ ⟨ ( 𝑧 ↾ 𝐴 ) , ( 𝑧 ↾ 𝐵 ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		ptunhmeo.x	⊢ 𝑋 = ∪ 𝐾
2		ptunhmeo.y	⊢ 𝑌 = ∪ 𝐿
3		ptunhmeo.j	⊢ 𝐽 = ( ∏_t ‘ 𝐹 )
4		ptunhmeo.k	⊢ 𝐾 = ( ∏_t ‘ ( 𝐹 ↾ 𝐴 ) )
5		ptunhmeo.l	⊢ 𝐿 = ( ∏_t ‘ ( 𝐹 ↾ 𝐵 ) )
6		ptunhmeo.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝑥 ∪ 𝑦 ) )
7		ptunhmeo.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8		ptunhmeo.f	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ Top )
9		ptunhmeo.u	⊢ ( 𝜑 → 𝐶 = ( 𝐴 ∪ 𝐵 ) )
10		ptunhmeo.i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
11		vex	⊢ 𝑥 ∈ V
12		vex	⊢ 𝑦 ∈ V
13	11 12	op1std	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑤 ) = 𝑥 )
14	11 12	op2ndd	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑤 ) = 𝑦 )
15	13 14	uneq12d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) = ( 𝑥 ∪ 𝑦 ) )
16	15	mpompt	⊢ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝑥 ∪ 𝑦 ) )
17	6 16	eqtr4i	⊢ 𝐺 = ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) )
18		xp1st	⊢ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) → ( 1^st ‘ 𝑤 ) ∈ 𝑋 )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 1^st ‘ 𝑤 ) ∈ 𝑋 )
20		ixpeq2	⊢ ( ∀ 𝑘 ∈ 𝐴 ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) → X 𝑘 ∈ 𝐴 ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) = X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
21		fvres	⊢ ( 𝑘 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
22	21	unieqd	⊢ ( 𝑘 ∈ 𝐴 → ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
23	20 22	mprg	⊢ X 𝑘 ∈ 𝐴 ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) = X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 )
24		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
25	24 9	sseqtrrid	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
26	7 25	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
27	8 25	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ Top )
28	4	ptuni	⊢ ( ( 𝐴 ∈ V ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ Top ) → X 𝑘 ∈ 𝐴 ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) = ∪ 𝐾 )
29	26 27 28	syl2anc	⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) = ∪ 𝐾 )
30	23 29	eqtr3id	⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐾 )
31	30 1	eqtr4di	⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = 𝑋 )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = 𝑋 )
33	19 32	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 1^st ‘ 𝑤 ) ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
34		xp2nd	⊢ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) → ( 2^nd ‘ 𝑤 ) ∈ 𝑌 )
35	34	adantl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑤 ) ∈ 𝑌 )
36	9	eqcomd	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) = 𝐶 )
37		uneqdifeq	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐴 ∪ 𝐵 ) = 𝐶 ↔ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
38	25 10 37	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐵 ) = 𝐶 ↔ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
39	36 38	mpbid	⊢ ( 𝜑 → ( 𝐶 ∖ 𝐴 ) = 𝐵 )
40	39	ixpeq1d	⊢ ( 𝜑 → X 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐹 ‘ 𝑘 ) = X 𝑘 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑘 ) )
41		ixpeq2	⊢ ( ∀ 𝑘 ∈ 𝐵 ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) → X 𝑘 ∈ 𝐵 ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) = X 𝑘 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑘 ) )
42		fvres	⊢ ( 𝑘 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
43	42	unieqd	⊢ ( 𝑘 ∈ 𝐵 → ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
44	41 43	mprg	⊢ X 𝑘 ∈ 𝐵 ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) = X 𝑘 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑘 )
45		ssun2	⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
46	45 9	sseqtrrid	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
47	7 46	ssexd	⊢ ( 𝜑 → 𝐵 ∈ V )
48	8 46	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ Top )
49	5	ptuni	⊢ ( ( 𝐵 ∈ V ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ Top ) → X 𝑘 ∈ 𝐵 ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) = ∪ 𝐿 )
50	47 48 49	syl2anc	⊢ ( 𝜑 → X 𝑘 ∈ 𝐵 ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) = ∪ 𝐿 )
51	44 50	eqtr3id	⊢ ( 𝜑 → X 𝑘 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐿 )
52	51 2	eqtr4di	⊢ ( 𝜑 → X 𝑘 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑘 ) = 𝑌 )
53	40 52	eqtrd	⊢ ( 𝜑 → X 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐹 ‘ 𝑘 ) = 𝑌 )
54	53	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐹 ‘ 𝑘 ) = 𝑌 )
55	35 54	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑤 ) ∈ X 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐹 ‘ 𝑘 ) )
56	25	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → 𝐴 ⊆ 𝐶 )
57		undifixp	⊢ ( ( ( 1^st ‘ 𝑤 ) ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 2^nd ‘ 𝑤 ) ∈ X 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐹 ‘ 𝑘 ) ∧ 𝐴 ⊆ 𝐶 ) → ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∈ X 𝑘 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑘 ) )
58	33 55 56 57	syl3anc	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∈ X 𝑘 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑘 ) )
59	3	ptuni	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 : 𝐶 ⟶ Top ) → X 𝑘 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐽 )
60	7 8 59	syl2anc	⊢ ( 𝜑 → X 𝑘 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐽 )
61	60	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑘 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐽 )
62	58 61	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∈ ∪ 𝐽 )
63	25	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐽 ) → 𝐴 ⊆ 𝐶 )
64	60	eleq2d	⊢ ( 𝜑 → ( 𝑧 ∈ X 𝑘 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑘 ) ↔ 𝑧 ∈ ∪ 𝐽 ) )
65	64	biimpar	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐽 ) → 𝑧 ∈ X 𝑘 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑘 ) )
66		resixp	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝑧 ∈ X 𝑘 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑧 ↾ 𝐴 ) ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
67	63 65 66	syl2anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐽 ) → ( 𝑧 ↾ 𝐴 ) ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
68	31	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐽 ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = 𝑋 )
69	67 68	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐽 ) → ( 𝑧 ↾ 𝐴 ) ∈ 𝑋 )
70	46	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐽 ) → 𝐵 ⊆ 𝐶 )
71		resixp	⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝑧 ∈ X 𝑘 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑧 ↾ 𝐵 ) ∈ X 𝑘 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑘 ) )
72	70 65 71	syl2anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐽 ) → ( 𝑧 ↾ 𝐵 ) ∈ X 𝑘 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑘 ) )
73	52	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐽 ) → X 𝑘 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑘 ) = 𝑌 )
74	72 73	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐽 ) → ( 𝑧 ↾ 𝐵 ) ∈ 𝑌 )
75	69 74	opelxpd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐽 ) → ⟨ ( 𝑧 ↾ 𝐴 ) , ( 𝑧 ↾ 𝐵 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
76		eqop	⊢ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) → ( 𝑤 = ⟨ ( 𝑧 ↾ 𝐴 ) , ( 𝑧 ↾ 𝐵 ) ⟩ ↔ ( ( 1^st ‘ 𝑤 ) = ( 𝑧 ↾ 𝐴 ) ∧ ( 2^nd ‘ 𝑤 ) = ( 𝑧 ↾ 𝐵 ) ) ) )
77	76	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 𝑤 = ⟨ ( 𝑧 ↾ 𝐴 ) , ( 𝑧 ↾ 𝐵 ) ⟩ ↔ ( ( 1^st ‘ 𝑤 ) = ( 𝑧 ↾ 𝐴 ) ∧ ( 2^nd ‘ 𝑤 ) = ( 𝑧 ↾ 𝐵 ) ) ) )
78	65	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → 𝑧 ∈ X 𝑘 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑘 ) )
79		ixpfn	⊢ ( 𝑧 ∈ X 𝑘 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑘 ) → 𝑧 Fn 𝐶 )
80		fnresdm	⊢ ( 𝑧 Fn 𝐶 → ( 𝑧 ↾ 𝐶 ) = 𝑧 )
81	78 79 80	3syl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 𝑧 ↾ 𝐶 ) = 𝑧 )
82	9	reseq2d	⊢ ( 𝜑 → ( 𝑧 ↾ 𝐶 ) = ( 𝑧 ↾ ( 𝐴 ∪ 𝐵 ) ) )
83	82	adantr	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 𝑧 ↾ 𝐶 ) = ( 𝑧 ↾ ( 𝐴 ∪ 𝐵 ) ) )
84	81 83	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → 𝑧 = ( 𝑧 ↾ ( 𝐴 ∪ 𝐵 ) ) )
85		resundi	⊢ ( 𝑧 ↾ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑧 ↾ 𝐴 ) ∪ ( 𝑧 ↾ 𝐵 ) )
86	84 85	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → 𝑧 = ( ( 𝑧 ↾ 𝐴 ) ∪ ( 𝑧 ↾ 𝐵 ) ) )
87		uneq12	⊢ ( ( ( 1^st ‘ 𝑤 ) = ( 𝑧 ↾ 𝐴 ) ∧ ( 2^nd ‘ 𝑤 ) = ( 𝑧 ↾ 𝐵 ) ) → ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) = ( ( 𝑧 ↾ 𝐴 ) ∪ ( 𝑧 ↾ 𝐵 ) ) )
88	87	eqeq2d	⊢ ( ( ( 1^st ‘ 𝑤 ) = ( 𝑧 ↾ 𝐴 ) ∧ ( 2^nd ‘ 𝑤 ) = ( 𝑧 ↾ 𝐵 ) ) → ( 𝑧 = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↔ 𝑧 = ( ( 𝑧 ↾ 𝐴 ) ∪ ( 𝑧 ↾ 𝐵 ) ) ) )
89	86 88	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( ( ( 1^st ‘ 𝑤 ) = ( 𝑧 ↾ 𝐴 ) ∧ ( 2^nd ‘ 𝑤 ) = ( 𝑧 ↾ 𝐵 ) ) → 𝑧 = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ) )
90		ixpfn	⊢ ( ( 1^st ‘ 𝑤 ) ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → ( 1^st ‘ 𝑤 ) Fn 𝐴 )
91	33 90	syl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 1^st ‘ 𝑤 ) Fn 𝐴 )
92	91	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 1^st ‘ 𝑤 ) Fn 𝐴 )
93		dffn2	⊢ ( ( 1^st ‘ 𝑤 ) Fn 𝐴 ↔ ( 1^st ‘ 𝑤 ) : 𝐴 ⟶ V )
94	92 93	sylib	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 1^st ‘ 𝑤 ) : 𝐴 ⟶ V )
95	52	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑘 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑘 ) = 𝑌 )
96	35 95	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑤 ) ∈ X 𝑘 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑘 ) )
97		ixpfn	⊢ ( ( 2^nd ‘ 𝑤 ) ∈ X 𝑘 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑘 ) → ( 2^nd ‘ 𝑤 ) Fn 𝐵 )
98	96 97	syl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑤 ) Fn 𝐵 )
99	98	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 2^nd ‘ 𝑤 ) Fn 𝐵 )
100		dffn2	⊢ ( ( 2^nd ‘ 𝑤 ) Fn 𝐵 ↔ ( 2^nd ‘ 𝑤 ) : 𝐵 ⟶ V )
101	99 100	sylib	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 2^nd ‘ 𝑤 ) : 𝐵 ⟶ V )
102		res0	⊢ ( ( 1^st ‘ 𝑤 ) ↾ ∅ ) = ∅
103		res0	⊢ ( ( 2^nd ‘ 𝑤 ) ↾ ∅ ) = ∅
104	102 103	eqtr4i	⊢ ( ( 1^st ‘ 𝑤 ) ↾ ∅ ) = ( ( 2^nd ‘ 𝑤 ) ↾ ∅ )
105	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
106	105	reseq2d	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( ( 1^st ‘ 𝑤 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 1^st ‘ 𝑤 ) ↾ ∅ ) )
107	105	reseq2d	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( ( 2^nd ‘ 𝑤 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑤 ) ↾ ∅ ) )
108	104 106 107	3eqtr4a	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( ( 1^st ‘ 𝑤 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑤 ) ↾ ( 𝐴 ∩ 𝐵 ) ) )
109		fresaunres1	⊢ ( ( ( 1^st ‘ 𝑤 ) : 𝐴 ⟶ V ∧ ( 2^nd ‘ 𝑤 ) : 𝐵 ⟶ V ∧ ( ( 1^st ‘ 𝑤 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑤 ) ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐴 ) = ( 1^st ‘ 𝑤 ) )
110	94 101 108 109	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐴 ) = ( 1^st ‘ 𝑤 ) )
111	110	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 1^st ‘ 𝑤 ) = ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐴 ) )
112		fresaunres2	⊢ ( ( ( 1^st ‘ 𝑤 ) : 𝐴 ⟶ V ∧ ( 2^nd ‘ 𝑤 ) : 𝐵 ⟶ V ∧ ( ( 1^st ‘ 𝑤 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑤 ) ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐵 ) = ( 2^nd ‘ 𝑤 ) )
113	94 101 108 112	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐵 ) = ( 2^nd ‘ 𝑤 ) )
114	113	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 2^nd ‘ 𝑤 ) = ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐵 ) )
115	111 114	jca	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( ( 1^st ‘ 𝑤 ) = ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐴 ) ∧ ( 2^nd ‘ 𝑤 ) = ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐵 ) ) )
116		reseq1	⊢ ( 𝑧 = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) → ( 𝑧 ↾ 𝐴 ) = ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐴 ) )
117	116	eqeq2d	⊢ ( 𝑧 = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) → ( ( 1^st ‘ 𝑤 ) = ( 𝑧 ↾ 𝐴 ) ↔ ( 1^st ‘ 𝑤 ) = ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐴 ) ) )
118		reseq1	⊢ ( 𝑧 = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) → ( 𝑧 ↾ 𝐵 ) = ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐵 ) )
119	118	eqeq2d	⊢ ( 𝑧 = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) → ( ( 2^nd ‘ 𝑤 ) = ( 𝑧 ↾ 𝐵 ) ↔ ( 2^nd ‘ 𝑤 ) = ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐵 ) ) )
120	117 119	anbi12d	⊢ ( 𝑧 = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) → ( ( ( 1^st ‘ 𝑤 ) = ( 𝑧 ↾ 𝐴 ) ∧ ( 2^nd ‘ 𝑤 ) = ( 𝑧 ↾ 𝐵 ) ) ↔ ( ( 1^st ‘ 𝑤 ) = ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐴 ) ∧ ( 2^nd ‘ 𝑤 ) = ( ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↾ 𝐵 ) ) ) )
121	115 120	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 𝑧 = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) → ( ( 1^st ‘ 𝑤 ) = ( 𝑧 ↾ 𝐴 ) ∧ ( 2^nd ‘ 𝑤 ) = ( 𝑧 ↾ 𝐵 ) ) ) )
122	89 121	impbid	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( ( ( 1^st ‘ 𝑤 ) = ( 𝑧 ↾ 𝐴 ) ∧ ( 2^nd ‘ 𝑤 ) = ( 𝑧 ↾ 𝐵 ) ) ↔ 𝑧 = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ) )
123	77 122	bitrd	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( 𝑤 = ⟨ ( 𝑧 ↾ 𝐴 ) , ( 𝑧 ↾ 𝐵 ) ⟩ ↔ 𝑧 = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ) )
124	17 62 75 123	f1ocnv2d	⊢ ( 𝜑 → ( 𝐺 : ( 𝑋 × 𝑌 ) –1-1-onto→ ∪ 𝐽 ∧ ^◡ 𝐺 = ( 𝑧 ∈ ∪ 𝐽 ↦ ⟨ ( 𝑧 ↾ 𝐴 ) , ( 𝑧 ↾ 𝐵 ) ⟩ ) ) )
125	124	simprd	⊢ ( 𝜑 → ^◡ 𝐺 = ( 𝑧 ∈ ∪ 𝐽 ↦ ⟨ ( 𝑧 ↾ 𝐴 ) , ( 𝑧 ↾ 𝐵 ) ⟩ ) )

Metamath Proof Explorer

Theorem ptuncnv

Proof