Metamath Proof Explorer


Theorem 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 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st𝑤 ) = 𝑥 )
14 11 12 op2ndd ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd𝑤 ) = 𝑦 )
15 13 14 uneq12d ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) = ( 𝑥𝑦 ) )
16 15 mpompt ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ) = ( 𝑥𝑋 , 𝑦𝑌 ↦ ( 𝑥𝑦 ) )
17 6 16 eqtr4i 𝐺 = ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) )
18 xp1st ( 𝑤 ∈ ( 𝑋 × 𝑌 ) → ( 1st𝑤 ) ∈ 𝑋 )
19 18 adantl ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 1st𝑤 ) ∈ 𝑋 )
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 ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 1st𝑤 ) ∈ X 𝑘𝐴 ( 𝐹𝑘 ) )
34 xp2nd ( 𝑤 ∈ ( 𝑋 × 𝑌 ) → ( 2nd𝑤 ) ∈ 𝑌 )
35 34 adantl ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 2nd𝑤 ) ∈ 𝑌 )
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 ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 2nd𝑤 ) ∈ X 𝑘 ∈ ( 𝐶𝐴 ) ( 𝐹𝑘 ) )
56 25 adantr ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → 𝐴𝐶 )
57 undifixp ( ( ( 1st𝑤 ) ∈ X 𝑘𝐴 ( 𝐹𝑘 ) ∧ ( 2nd𝑤 ) ∈ X 𝑘 ∈ ( 𝐶𝐴 ) ( 𝐹𝑘 ) ∧ 𝐴𝐶 ) → ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ∈ X 𝑘𝐶 ( 𝐹𝑘 ) )
58 33 55 56 57 syl3anc ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ∈ X 𝑘𝐶 ( 𝐹𝑘 ) )
59 3 ptuni ( ( 𝐶𝑉𝐹 : 𝐶 ⟶ Top ) → X 𝑘𝐶 ( 𝐹𝑘 ) = 𝐽 )
60 7 8 59 syl2anc ( 𝜑X 𝑘𝐶 ( 𝐹𝑘 ) = 𝐽 )
61 60 adantr ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑘𝐶 ( 𝐹𝑘 ) = 𝐽 )
62 58 61 eleqtrd ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ∈ 𝐽 )
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 ( 𝑤 ∈ ( 𝑋 × 𝑌 ) → ( 𝑤 = ⟨ ( 𝑧𝐴 ) , ( 𝑧𝐵 ) ⟩ ↔ ( ( 1st𝑤 ) = ( 𝑧𝐴 ) ∧ ( 2nd𝑤 ) = ( 𝑧𝐵 ) ) ) )
77 76 ad2antrl ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( 𝑤 = ⟨ ( 𝑧𝐴 ) , ( 𝑧𝐵 ) ⟩ ↔ ( ( 1st𝑤 ) = ( 𝑧𝐴 ) ∧ ( 2nd𝑤 ) = ( 𝑧𝐵 ) ) ) )
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 ( ( ( 1st𝑤 ) = ( 𝑧𝐴 ) ∧ ( 2nd𝑤 ) = ( 𝑧𝐵 ) ) → ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) = ( ( 𝑧𝐴 ) ∪ ( 𝑧𝐵 ) ) )
88 87 eqeq2d ( ( ( 1st𝑤 ) = ( 𝑧𝐴 ) ∧ ( 2nd𝑤 ) = ( 𝑧𝐵 ) ) → ( 𝑧 = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↔ 𝑧 = ( ( 𝑧𝐴 ) ∪ ( 𝑧𝐵 ) ) ) )
89 86 88 syl5ibrcom ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( ( ( 1st𝑤 ) = ( 𝑧𝐴 ) ∧ ( 2nd𝑤 ) = ( 𝑧𝐵 ) ) → 𝑧 = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ) )
90 ixpfn ( ( 1st𝑤 ) ∈ X 𝑘𝐴 ( 𝐹𝑘 ) → ( 1st𝑤 ) Fn 𝐴 )
91 33 90 syl ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 1st𝑤 ) Fn 𝐴 )
92 91 adantrr ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( 1st𝑤 ) Fn 𝐴 )
93 dffn2 ( ( 1st𝑤 ) Fn 𝐴 ↔ ( 1st𝑤 ) : 𝐴 ⟶ V )
94 92 93 sylib ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( 1st𝑤 ) : 𝐴 ⟶ V )
95 52 adantr ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑘𝐵 ( 𝐹𝑘 ) = 𝑌 )
96 35 95 eleqtrrd ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 2nd𝑤 ) ∈ X 𝑘𝐵 ( 𝐹𝑘 ) )
97 ixpfn ( ( 2nd𝑤 ) ∈ X 𝑘𝐵 ( 𝐹𝑘 ) → ( 2nd𝑤 ) Fn 𝐵 )
98 96 97 syl ( ( 𝜑𝑤 ∈ ( 𝑋 × 𝑌 ) ) → ( 2nd𝑤 ) Fn 𝐵 )
99 98 adantrr ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( 2nd𝑤 ) Fn 𝐵 )
100 dffn2 ( ( 2nd𝑤 ) Fn 𝐵 ↔ ( 2nd𝑤 ) : 𝐵 ⟶ V )
101 99 100 sylib ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( 2nd𝑤 ) : 𝐵 ⟶ V )
102 res0 ( ( 1st𝑤 ) ↾ ∅ ) = ∅
103 res0 ( ( 2nd𝑤 ) ↾ ∅ ) = ∅
104 102 103 eqtr4i ( ( 1st𝑤 ) ↾ ∅ ) = ( ( 2nd𝑤 ) ↾ ∅ )
105 10 adantr ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( 𝐴𝐵 ) = ∅ )
106 105 reseq2d ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( ( 1st𝑤 ) ↾ ( 𝐴𝐵 ) ) = ( ( 1st𝑤 ) ↾ ∅ ) )
107 105 reseq2d ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( ( 2nd𝑤 ) ↾ ( 𝐴𝐵 ) ) = ( ( 2nd𝑤 ) ↾ ∅ ) )
108 104 106 107 3eqtr4a ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( ( 1st𝑤 ) ↾ ( 𝐴𝐵 ) ) = ( ( 2nd𝑤 ) ↾ ( 𝐴𝐵 ) ) )
109 fresaunres1 ( ( ( 1st𝑤 ) : 𝐴 ⟶ V ∧ ( 2nd𝑤 ) : 𝐵 ⟶ V ∧ ( ( 1st𝑤 ) ↾ ( 𝐴𝐵 ) ) = ( ( 2nd𝑤 ) ↾ ( 𝐴𝐵 ) ) ) → ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐴 ) = ( 1st𝑤 ) )
110 94 101 108 109 syl3anc ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐴 ) = ( 1st𝑤 ) )
111 110 eqcomd ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( 1st𝑤 ) = ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐴 ) )
112 fresaunres2 ( ( ( 1st𝑤 ) : 𝐴 ⟶ V ∧ ( 2nd𝑤 ) : 𝐵 ⟶ V ∧ ( ( 1st𝑤 ) ↾ ( 𝐴𝐵 ) ) = ( ( 2nd𝑤 ) ↾ ( 𝐴𝐵 ) ) ) → ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐵 ) = ( 2nd𝑤 ) )
113 94 101 108 112 syl3anc ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐵 ) = ( 2nd𝑤 ) )
114 113 eqcomd ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( 2nd𝑤 ) = ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐵 ) )
115 111 114 jca ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( ( 1st𝑤 ) = ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐴 ) ∧ ( 2nd𝑤 ) = ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐵 ) ) )
116 reseq1 ( 𝑧 = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) → ( 𝑧𝐴 ) = ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐴 ) )
117 116 eqeq2d ( 𝑧 = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) → ( ( 1st𝑤 ) = ( 𝑧𝐴 ) ↔ ( 1st𝑤 ) = ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐴 ) ) )
118 reseq1 ( 𝑧 = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) → ( 𝑧𝐵 ) = ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐵 ) )
119 118 eqeq2d ( 𝑧 = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) → ( ( 2nd𝑤 ) = ( 𝑧𝐵 ) ↔ ( 2nd𝑤 ) = ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐵 ) ) )
120 117 119 anbi12d ( 𝑧 = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) → ( ( ( 1st𝑤 ) = ( 𝑧𝐴 ) ∧ ( 2nd𝑤 ) = ( 𝑧𝐵 ) ) ↔ ( ( 1st𝑤 ) = ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐴 ) ∧ ( 2nd𝑤 ) = ( ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ↾ 𝐵 ) ) ) )
121 115 120 syl5ibrcom ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( 𝑧 = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) → ( ( 1st𝑤 ) = ( 𝑧𝐴 ) ∧ ( 2nd𝑤 ) = ( 𝑧𝐵 ) ) ) )
122 89 121 impbid ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( ( ( 1st𝑤 ) = ( 𝑧𝐴 ) ∧ ( 2nd𝑤 ) = ( 𝑧𝐵 ) ) ↔ 𝑧 = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ) )
123 77 122 bitrd ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝐽 ) ) → ( 𝑤 = ⟨ ( 𝑧𝐴 ) , ( 𝑧𝐵 ) ⟩ ↔ 𝑧 = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ) )
124 17 62 75 123 f1ocnv2d ( 𝜑 → ( 𝐺 : ( 𝑋 × 𝑌 ) –1-1-onto 𝐽 𝐺 = ( 𝑧 𝐽 ↦ ⟨ ( 𝑧𝐴 ) , ( 𝑧𝐵 ) ⟩ ) ) )
125 124 simprd ( 𝜑 𝐺 = ( 𝑧 𝐽 ↦ ⟨ ( 𝑧𝐴 ) , ( 𝑧𝐵 ) ⟩ ) )