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	$⊢ X = ⋃ K$
	ptunhmeo.y	$⊢ Y = ⋃ L$
	ptunhmeo.j	$⊢ J = \prod_{𝑡} (F)$
	ptunhmeo.k	$⊢ K = \prod_{𝑡} ({F ↾}_{A})$
	ptunhmeo.l	$⊢ L = \prod_{𝑡} ({F ↾}_{B})$
	ptunhmeo.g	$⊢ G = (x \in X, y \in Y ⟼ x \cup y)$
	ptunhmeo.c	$⊢ φ \to C \in V$
	ptunhmeo.f	$⊢ φ \to F : C ⟶ Top$
	ptunhmeo.u	$⊢ φ \to C = A \cup B$
	ptunhmeo.i	$⊢ φ \to A \cap B = \emptyset$
Assertion	ptuncnv	$⊢ φ \to G^{-1} = (z \in ⋃ J ⟼ ⟨{z ↾}_{A}, {z ↾}_{B}⟩)$

Proof

Step	Hyp	Ref	Expression
1		ptunhmeo.x	$⊢ X = ⋃ K$
2		ptunhmeo.y	$⊢ Y = ⋃ L$
3		ptunhmeo.j	$⊢ J = \prod_{𝑡} (F)$
4		ptunhmeo.k	$⊢ K = \prod_{𝑡} ({F ↾}_{A})$
5		ptunhmeo.l	$⊢ L = \prod_{𝑡} ({F ↾}_{B})$
6		ptunhmeo.g	$⊢ G = (x \in X, y \in Y ⟼ x \cup y)$
7		ptunhmeo.c	$⊢ φ \to C \in V$
8		ptunhmeo.f	$⊢ φ \to F : C ⟶ Top$
9		ptunhmeo.u	$⊢ φ \to C = A \cup B$
10		ptunhmeo.i	$⊢ φ \to A \cap B = \emptyset$
11		vex	$⊢ x \in V$
12		vex	$⊢ y \in V$
13	11 12	op1std	$⊢ w = ⟨x, y⟩ \to 1^{st} (w) = x$
14	11 12	op2ndd	$⊢ w = ⟨x, y⟩ \to 2^{nd} (w) = y$
15	13 14	uneq12d	$⊢ w = ⟨x, y⟩ \to 1^{st} (w) \cup 2^{nd} (w) = x \cup y$
16	15	mpompt	$⊢ (w \in (X \times Y) ⟼ 1^{st} (w) \cup 2^{nd} (w)) = (x \in X, y \in Y ⟼ x \cup y)$
17	6 16	eqtr4i	$⊢ G = (w \in (X \times Y) ⟼ 1^{st} (w) \cup 2^{nd} (w))$
18		xp1st	$⊢ w \in (X \times Y) \to 1^{st} (w) \in X$
19	18	adantl	$⊢ (φ \land w \in (X \times Y)) \to 1^{st} (w) \in X$
20		ixpeq2	$⊢ \forall k \in A ⋃ ({F ↾}_{A}) (k) = ⋃ F (k) \to \underset{k \in A}{⨉} ⋃ ({F ↾}_{A}) (k) = \underset{k \in A}{⨉} ⋃ F (k)$
21		fvres	$⊢ k \in A \to ({F ↾}_{A}) (k) = F (k)$
22	21	unieqd	$⊢ k \in A \to ⋃ ({F ↾}_{A}) (k) = ⋃ F (k)$
23	20 22	mprg	$⊢ \underset{k \in A}{⨉} ⋃ ({F ↾}_{A}) (k) = \underset{k \in A}{⨉} ⋃ F (k)$
24		ssun1	$⊢ A \subseteq A \cup B$
25	24 9	sseqtrrid	$⊢ φ \to A \subseteq C$
26	7 25	ssexd	$⊢ φ \to A \in V$
27	8 25	fssresd	$⊢ φ \to ({F ↾}_{A}) : A ⟶ Top$
28	4	ptuni	$⊢ (A \in V \land ({F ↾}_{A}) : A ⟶ Top) \to \underset{k \in A}{⨉} ⋃ ({F ↾}_{A}) (k) = ⋃ K$
29	26 27 28	syl2anc	$⊢ φ \to \underset{k \in A}{⨉} ⋃ ({F ↾}_{A}) (k) = ⋃ K$
30	23 29	syl5eqr	$⊢ φ \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ K$
31	30 1	syl6eqr	$⊢ φ \to \underset{k \in A}{⨉} ⋃ F (k) = X$
32	31	adantr	$⊢ (φ \land w \in (X \times Y)) \to \underset{k \in A}{⨉} ⋃ F (k) = X$
33	19 32	eleqtrrd	$⊢ (φ \land w \in (X \times Y)) \to 1^{st} (w) \in \underset{k \in A}{⨉} ⋃ F (k)$
34		xp2nd	$⊢ w \in (X \times Y) \to 2^{nd} (w) \in Y$
35	34	adantl	$⊢ (φ \land w \in (X \times Y)) \to 2^{nd} (w) \in Y$
36	9	eqcomd	$⊢ φ \to A \cup B = C$
37		uneqdifeq	$⊢ (A \subseteq C \land A \cap B = \emptyset) \to (A \cup B = C \leftrightarrow C ∖ A = B)$
38	25 10 37	syl2anc	$⊢ φ \to (A \cup B = C \leftrightarrow C ∖ A = B)$
39	36 38	mpbid	$⊢ φ \to C ∖ A = B$
40	39	ixpeq1d	$⊢ φ \to \underset{k \in C ∖ A}{⨉} ⋃ F (k) = \underset{k \in B}{⨉} ⋃ F (k)$
41		ixpeq2	$⊢ \forall k \in B ⋃ ({F ↾}_{B}) (k) = ⋃ F (k) \to \underset{k \in B}{⨉} ⋃ ({F ↾}_{B}) (k) = \underset{k \in B}{⨉} ⋃ F (k)$
42		fvres	$⊢ k \in B \to ({F ↾}_{B}) (k) = F (k)$
43	42	unieqd	$⊢ k \in B \to ⋃ ({F ↾}_{B}) (k) = ⋃ F (k)$
44	41 43	mprg	$⊢ \underset{k \in B}{⨉} ⋃ ({F ↾}_{B}) (k) = \underset{k \in B}{⨉} ⋃ F (k)$
45		ssun2	$⊢ B \subseteq A \cup B$
46	45 9	sseqtrrid	$⊢ φ \to B \subseteq C$
47	7 46	ssexd	$⊢ φ \to B \in V$
48	8 46	fssresd	$⊢ φ \to ({F ↾}_{B}) : B ⟶ Top$
49	5	ptuni	$⊢ (B \in V \land ({F ↾}_{B}) : B ⟶ Top) \to \underset{k \in B}{⨉} ⋃ ({F ↾}_{B}) (k) = ⋃ L$
50	47 48 49	syl2anc	$⊢ φ \to \underset{k \in B}{⨉} ⋃ ({F ↾}_{B}) (k) = ⋃ L$
51	44 50	syl5eqr	$⊢ φ \to \underset{k \in B}{⨉} ⋃ F (k) = ⋃ L$
52	51 2	syl6eqr	$⊢ φ \to \underset{k \in B}{⨉} ⋃ F (k) = Y$
53	40 52	eqtrd	$⊢ φ \to \underset{k \in C ∖ A}{⨉} ⋃ F (k) = Y$
54	53	adantr	$⊢ (φ \land w \in (X \times Y)) \to \underset{k \in C ∖ A}{⨉} ⋃ F (k) = Y$
55	35 54	eleqtrrd	$⊢ (φ \land w \in (X \times Y)) \to 2^{nd} (w) \in \underset{k \in C ∖ A}{⨉} ⋃ F (k)$
56	25	adantr	$⊢ (φ \land w \in (X \times Y)) \to A \subseteq C$
57		undifixp	$⊢ (1^{st} (w) \in \underset{k \in A}{⨉} ⋃ F (k) \land 2^{nd} (w) \in \underset{k \in C ∖ A}{⨉} ⋃ F (k) \land A \subseteq C) \to 1^{st} (w) \cup 2^{nd} (w) \in \underset{k \in C}{⨉} ⋃ F (k)$
58	33 55 56 57	syl3anc	$⊢ (φ \land w \in (X \times Y)) \to 1^{st} (w) \cup 2^{nd} (w) \in \underset{k \in C}{⨉} ⋃ F (k)$
59	3	ptuni	$⊢ (C \in V \land F : C ⟶ Top) \to \underset{k \in C}{⨉} ⋃ F (k) = ⋃ J$
60	7 8 59	syl2anc	$⊢ φ \to \underset{k \in C}{⨉} ⋃ F (k) = ⋃ J$
61	60	adantr	$⊢ (φ \land w \in (X \times Y)) \to \underset{k \in C}{⨉} ⋃ F (k) = ⋃ J$
62	58 61	eleqtrd	$⊢ (φ \land w \in (X \times Y)) \to 1^{st} (w) \cup 2^{nd} (w) \in ⋃ J$
63	25	adantr	$⊢ (φ \land z \in ⋃ J) \to A \subseteq C$
64	60	eleq2d	$⊢ φ \to (z \in \underset{k \in C}{⨉} ⋃ F (k) \leftrightarrow z \in ⋃ J)$
65	64	biimpar	$⊢ (φ \land z \in ⋃ J) \to z \in \underset{k \in C}{⨉} ⋃ F (k)$
66		resixp	$⊢ (A \subseteq C \land z \in \underset{k \in C}{⨉} ⋃ F (k)) \to {z ↾}_{A} \in \underset{k \in A}{⨉} ⋃ F (k)$
67	63 65 66	syl2anc	$⊢ (φ \land z \in ⋃ J) \to {z ↾}_{A} \in \underset{k \in A}{⨉} ⋃ F (k)$
68	31	adantr	$⊢ (φ \land z \in ⋃ J) \to \underset{k \in A}{⨉} ⋃ F (k) = X$
69	67 68	eleqtrd	$⊢ (φ \land z \in ⋃ J) \to {z ↾}_{A} \in X$
70	46	adantr	$⊢ (φ \land z \in ⋃ J) \to B \subseteq C$
71		resixp	$⊢ (B \subseteq C \land z \in \underset{k \in C}{⨉} ⋃ F (k)) \to {z ↾}_{B} \in \underset{k \in B}{⨉} ⋃ F (k)$
72	70 65 71	syl2anc	$⊢ (φ \land z \in ⋃ J) \to {z ↾}_{B} \in \underset{k \in B}{⨉} ⋃ F (k)$
73	52	adantr	$⊢ (φ \land z \in ⋃ J) \to \underset{k \in B}{⨉} ⋃ F (k) = Y$
74	72 73	eleqtrd	$⊢ (φ \land z \in ⋃ J) \to {z ↾}_{B} \in Y$
75	69 74	opelxpd	$⊢ (φ \land z \in ⋃ J) \to ⟨{z ↾}_{A}, {z ↾}_{B}⟩ \in (X \times Y)$
76		eqop	$⊢ w \in (X \times Y) \to (w = ⟨{z ↾}_{A}, {z ↾}_{B}⟩ \leftrightarrow (1^{st} (w) = {z ↾}_{A} \land 2^{nd} (w) = {z ↾}_{B}))$
77	76	ad2antrl	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to (w = ⟨{z ↾}_{A}, {z ↾}_{B}⟩ \leftrightarrow (1^{st} (w) = {z ↾}_{A} \land 2^{nd} (w) = {z ↾}_{B}))$
78	65	adantrl	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to z \in \underset{k \in C}{⨉} ⋃ F (k)$
79		ixpfn	$⊢ z \in \underset{k \in C}{⨉} ⋃ F (k) \to z Fn C$
80		fnresdm	$⊢ z Fn C \to {z ↾}_{C} = z$
81	78 79 80	3syl	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to {z ↾}_{C} = z$
82	9	reseq2d	$⊢ φ \to {z ↾}_{C} = {z ↾}_{(A \cup B)}$
83	82	adantr	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to {z ↾}_{C} = {z ↾}_{(A \cup B)}$
84	81 83	eqtr3d	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to z = {z ↾}_{(A \cup B)}$
85		resundi	$⊢ {z ↾}_{(A \cup B)} = ({z ↾}_{A}) \cup ({z ↾}_{B})$
86	84 85	syl6eq	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to z = ({z ↾}_{A}) \cup ({z ↾}_{B})$
87		uneq12	$⊢ (1^{st} (w) = {z ↾}_{A} \land 2^{nd} (w) = {z ↾}_{B}) \to 1^{st} (w) \cup 2^{nd} (w) = ({z ↾}_{A}) \cup ({z ↾}_{B})$
88	87	eqeq2d	$⊢ (1^{st} (w) = {z ↾}_{A} \land 2^{nd} (w) = {z ↾}_{B}) \to (z = 1^{st} (w) \cup 2^{nd} (w) \leftrightarrow z = ({z ↾}_{A}) \cup ({z ↾}_{B}))$
89	86 88	syl5ibrcom	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to ((1^{st} (w) = {z ↾}_{A} \land 2^{nd} (w) = {z ↾}_{B}) \to z = 1^{st} (w) \cup 2^{nd} (w))$
90		ixpfn	$⊢ 1^{st} (w) \in \underset{k \in A}{⨉} ⋃ F (k) \to 1^{st} (w) Fn A$
91	33 90	syl	$⊢ (φ \land w \in (X \times Y)) \to 1^{st} (w) Fn A$
92	91	adantrr	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to 1^{st} (w) Fn A$
93		dffn2	$⊢ 1^{st} (w) Fn A \leftrightarrow 1^{st} (w) : A ⟶ V$
94	92 93	sylib	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to 1^{st} (w) : A ⟶ V$
95	52	adantr	$⊢ (φ \land w \in (X \times Y)) \to \underset{k \in B}{⨉} ⋃ F (k) = Y$
96	35 95	eleqtrrd	$⊢ (φ \land w \in (X \times Y)) \to 2^{nd} (w) \in \underset{k \in B}{⨉} ⋃ F (k)$
97		ixpfn	$⊢ 2^{nd} (w) \in \underset{k \in B}{⨉} ⋃ F (k) \to 2^{nd} (w) Fn B$
98	96 97	syl	$⊢ (φ \land w \in (X \times Y)) \to 2^{nd} (w) Fn B$
99	98	adantrr	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to 2^{nd} (w) Fn B$
100		dffn2	$⊢ 2^{nd} (w) Fn B \leftrightarrow 2^{nd} (w) : B ⟶ V$
101	99 100	sylib	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to 2^{nd} (w) : B ⟶ V$
102		res0	$⊢ {1^{st} (w) ↾}_{\emptyset} = \emptyset$
103		res0	$⊢ {2^{nd} (w) ↾}_{\emptyset} = \emptyset$
104	102 103	eqtr4i	$⊢ {1^{st} (w) ↾}_{\emptyset} = {2^{nd} (w) ↾}_{\emptyset}$
105	10	adantr	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to A \cap B = \emptyset$
106	105	reseq2d	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to {1^{st} (w) ↾}_{(A \cap B)} = {1^{st} (w) ↾}_{\emptyset}$
107	105	reseq2d	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to {2^{nd} (w) ↾}_{(A \cap B)} = {2^{nd} (w) ↾}_{\emptyset}$
108	104 106 107	3eqtr4a	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to {1^{st} (w) ↾}_{(A \cap B)} = {2^{nd} (w) ↾}_{(A \cap B)}$
109		fresaunres1	$⊢ (1^{st} (w) : A ⟶ V \land 2^{nd} (w) : B ⟶ V \land {1^{st} (w) ↾}_{(A \cap B)} = {2^{nd} (w) ↾}_{(A \cap B)}) \to {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{A} = 1^{st} (w)$
110	94 101 108 109	syl3anc	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{A} = 1^{st} (w)$
111	110	eqcomd	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to 1^{st} (w) = {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{A}$
112		fresaunres2	$⊢ (1^{st} (w) : A ⟶ V \land 2^{nd} (w) : B ⟶ V \land {1^{st} (w) ↾}_{(A \cap B)} = {2^{nd} (w) ↾}_{(A \cap B)}) \to {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{B} = 2^{nd} (w)$
113	94 101 108 112	syl3anc	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{B} = 2^{nd} (w)$
114	113	eqcomd	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to 2^{nd} (w) = {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{B}$
115	111 114	jca	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to (1^{st} (w) = {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{A} \land 2^{nd} (w) = {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{B})$
116		reseq1	$⊢ z = 1^{st} (w) \cup 2^{nd} (w) \to {z ↾}_{A} = {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{A}$
117	116	eqeq2d	$⊢ z = 1^{st} (w) \cup 2^{nd} (w) \to (1^{st} (w) = {z ↾}_{A} \leftrightarrow 1^{st} (w) = {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{A})$
118		reseq1	$⊢ z = 1^{st} (w) \cup 2^{nd} (w) \to {z ↾}_{B} = {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{B}$
119	118	eqeq2d	$⊢ z = 1^{st} (w) \cup 2^{nd} (w) \to (2^{nd} (w) = {z ↾}_{B} \leftrightarrow 2^{nd} (w) = {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{B})$
120	117 119	anbi12d	$⊢ z = 1^{st} (w) \cup 2^{nd} (w) \to ((1^{st} (w) = {z ↾}_{A} \land 2^{nd} (w) = {z ↾}_{B}) \leftrightarrow (1^{st} (w) = {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{A} \land 2^{nd} (w) = {(1^{st} (w) \cup 2^{nd} (w)) ↾}_{B}))$
121	115 120	syl5ibrcom	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to (z = 1^{st} (w) \cup 2^{nd} (w) \to (1^{st} (w) = {z ↾}_{A} \land 2^{nd} (w) = {z ↾}_{B}))$
122	89 121	impbid	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to ((1^{st} (w) = {z ↾}_{A} \land 2^{nd} (w) = {z ↾}_{B}) \leftrightarrow z = 1^{st} (w) \cup 2^{nd} (w))$
123	77 122	bitrd	$⊢ (φ \land (w \in (X \times Y) \land z \in ⋃ J)) \to (w = ⟨{z ↾}_{A}, {z ↾}_{B}⟩ \leftrightarrow z = 1^{st} (w) \cup 2^{nd} (w))$
124	17 62 75 123	f1ocnv2d	$⊢ φ \to (G : X \times Y \underset{1-1 onto}{⟶} ⋃ J \land G^{-1} = (z \in ⋃ J ⟼ ⟨{z ↾}_{A}, {z ↾}_{B}⟩))$
125	124	simprd	$⊢ φ \to G^{-1} = (z \in ⋃ J ⟼ ⟨{z ↾}_{A}, {z ↾}_{B}⟩)$

Metamath Proof Explorer

Theorem ptuncnv

Proof