MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ptuncnv Structured version   Visualization version   GIF version

Theorem ptuncnv 21515
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.
StepHypRef Expression
1 ptunhmeo.g . . . 4 𝐺 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑦))
2 vex 3194 . . . . . . 7 𝑥 ∈ V
3 vex 3194 . . . . . . 7 𝑦 ∈ V
42, 3op1std 7126 . . . . . 6 (𝑤 = ⟨𝑥, 𝑦⟩ → (1st𝑤) = 𝑥)
52, 3op2ndd 7127 . . . . . 6 (𝑤 = ⟨𝑥, 𝑦⟩ → (2nd𝑤) = 𝑦)
64, 5uneq12d 3751 . . . . 5 (𝑤 = ⟨𝑥, 𝑦⟩ → ((1st𝑤) ∪ (2nd𝑤)) = (𝑥𝑦))
76mpt2mpt 6706 . . . 4 (𝑤 ∈ (𝑋 × 𝑌) ↦ ((1st𝑤) ∪ (2nd𝑤))) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑦))
81, 7eqtr4i 2651 . . 3 𝐺 = (𝑤 ∈ (𝑋 × 𝑌) ↦ ((1st𝑤) ∪ (2nd𝑤)))
9 xp1st 7146 . . . . . . 7 (𝑤 ∈ (𝑋 × 𝑌) → (1st𝑤) ∈ 𝑋)
109adantl 482 . . . . . 6 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → (1st𝑤) ∈ 𝑋)
11 ixpeq2 7867 . . . . . . . . . 10 (∀𝑘𝐴 ((𝐹𝐴)‘𝑘) = (𝐹𝑘) → X𝑘𝐴 ((𝐹𝐴)‘𝑘) = X𝑘𝐴 (𝐹𝑘))
12 fvres 6165 . . . . . . . . . . 11 (𝑘𝐴 → ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
1312unieqd 4417 . . . . . . . . . 10 (𝑘𝐴 ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
1411, 13mprg 2926 . . . . . . . . 9 X𝑘𝐴 ((𝐹𝐴)‘𝑘) = X𝑘𝐴 (𝐹𝑘)
15 ptunhmeo.c . . . . . . . . . . 11 (𝜑𝐶𝑉)
16 ssun1 3759 . . . . . . . . . . . 12 𝐴 ⊆ (𝐴𝐵)
17 ptunhmeo.u . . . . . . . . . . . 12 (𝜑𝐶 = (𝐴𝐵))
1816, 17syl5sseqr 3638 . . . . . . . . . . 11 (𝜑𝐴𝐶)
1915, 18ssexd 4770 . . . . . . . . . 10 (𝜑𝐴 ∈ V)
20 ptunhmeo.f . . . . . . . . . . 11 (𝜑𝐹:𝐶⟶Top)
2120, 18fssresd 6030 . . . . . . . . . 10 (𝜑 → (𝐹𝐴):𝐴⟶Top)
22 ptunhmeo.k . . . . . . . . . . 11 𝐾 = (∏t‘(𝐹𝐴))
2322ptuni 21302 . . . . . . . . . 10 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top) → X𝑘𝐴 ((𝐹𝐴)‘𝑘) = 𝐾)
2419, 21, 23syl2anc 692 . . . . . . . . 9 (𝜑X𝑘𝐴 ((𝐹𝐴)‘𝑘) = 𝐾)
2514, 24syl5eqr 2674 . . . . . . . 8 (𝜑X𝑘𝐴 (𝐹𝑘) = 𝐾)
26 ptunhmeo.x . . . . . . . 8 𝑋 = 𝐾
2725, 26syl6eqr 2678 . . . . . . 7 (𝜑X𝑘𝐴 (𝐹𝑘) = 𝑋)
2827adantr 481 . . . . . 6 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → X𝑘𝐴 (𝐹𝑘) = 𝑋)
2910, 28eleqtrrd 2707 . . . . 5 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → (1st𝑤) ∈ X𝑘𝐴 (𝐹𝑘))
30 xp2nd 7147 . . . . . . 7 (𝑤 ∈ (𝑋 × 𝑌) → (2nd𝑤) ∈ 𝑌)
3130adantl 482 . . . . . 6 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → (2nd𝑤) ∈ 𝑌)
3217eqcomd 2632 . . . . . . . . . 10 (𝜑 → (𝐴𝐵) = 𝐶)
33 ptunhmeo.i . . . . . . . . . . 11 (𝜑 → (𝐴𝐵) = ∅)
34 uneqdifeq 4034 . . . . . . . . . . 11 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3518, 33, 34syl2anc 692 . . . . . . . . . 10 (𝜑 → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3632, 35mpbid 222 . . . . . . . . 9 (𝜑 → (𝐶𝐴) = 𝐵)
3736ixpeq1d 7865 . . . . . . . 8 (𝜑X𝑘 ∈ (𝐶𝐴) (𝐹𝑘) = X𝑘𝐵 (𝐹𝑘))
38 ixpeq2 7867 . . . . . . . . . . 11 (∀𝑘𝐵 ((𝐹𝐵)‘𝑘) = (𝐹𝑘) → X𝑘𝐵 ((𝐹𝐵)‘𝑘) = X𝑘𝐵 (𝐹𝑘))
39 fvres 6165 . . . . . . . . . . . 12 (𝑘𝐵 → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
4039unieqd 4417 . . . . . . . . . . 11 (𝑘𝐵 ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
4138, 40mprg 2926 . . . . . . . . . 10 X𝑘𝐵 ((𝐹𝐵)‘𝑘) = X𝑘𝐵 (𝐹𝑘)
42 ssun2 3760 . . . . . . . . . . . . 13 𝐵 ⊆ (𝐴𝐵)
4342, 17syl5sseqr 3638 . . . . . . . . . . . 12 (𝜑𝐵𝐶)
4415, 43ssexd 4770 . . . . . . . . . . 11 (𝜑𝐵 ∈ V)
4520, 43fssresd 6030 . . . . . . . . . . 11 (𝜑 → (𝐹𝐵):𝐵⟶Top)
46 ptunhmeo.l . . . . . . . . . . . 12 𝐿 = (∏t‘(𝐹𝐵))
4746ptuni 21302 . . . . . . . . . . 11 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → X𝑘𝐵 ((𝐹𝐵)‘𝑘) = 𝐿)
4844, 45, 47syl2anc 692 . . . . . . . . . 10 (𝜑X𝑘𝐵 ((𝐹𝐵)‘𝑘) = 𝐿)
4941, 48syl5eqr 2674 . . . . . . . . 9 (𝜑X𝑘𝐵 (𝐹𝑘) = 𝐿)
50 ptunhmeo.y . . . . . . . . 9 𝑌 = 𝐿
5149, 50syl6eqr 2678 . . . . . . . 8 (𝜑X𝑘𝐵 (𝐹𝑘) = 𝑌)
5237, 51eqtrd 2660 . . . . . . 7 (𝜑X𝑘 ∈ (𝐶𝐴) (𝐹𝑘) = 𝑌)
5352adantr 481 . . . . . 6 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → X𝑘 ∈ (𝐶𝐴) (𝐹𝑘) = 𝑌)
5431, 53eleqtrrd 2707 . . . . 5 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → (2nd𝑤) ∈ X𝑘 ∈ (𝐶𝐴) (𝐹𝑘))
5518adantr 481 . . . . 5 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → 𝐴𝐶)
56 undifixp 7889 . . . . 5 (((1st𝑤) ∈ X𝑘𝐴 (𝐹𝑘) ∧ (2nd𝑤) ∈ X𝑘 ∈ (𝐶𝐴) (𝐹𝑘) ∧ 𝐴𝐶) → ((1st𝑤) ∪ (2nd𝑤)) ∈ X𝑘𝐶 (𝐹𝑘))
5729, 54, 55, 56syl3anc 1323 . . . 4 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → ((1st𝑤) ∪ (2nd𝑤)) ∈ X𝑘𝐶 (𝐹𝑘))
58 ptunhmeo.j . . . . . . 7 𝐽 = (∏t𝐹)
5958ptuni 21302 . . . . . 6 ((𝐶𝑉𝐹:𝐶⟶Top) → X𝑘𝐶 (𝐹𝑘) = 𝐽)
6015, 20, 59syl2anc 692 . . . . 5 (𝜑X𝑘𝐶 (𝐹𝑘) = 𝐽)
6160adantr 481 . . . 4 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → X𝑘𝐶 (𝐹𝑘) = 𝐽)
6257, 61eleqtrd 2706 . . 3 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝐽)
6318adantr 481 . . . . . 6 ((𝜑𝑧 𝐽) → 𝐴𝐶)
6460eleq2d 2689 . . . . . . 7 (𝜑 → (𝑧X𝑘𝐶 (𝐹𝑘) ↔ 𝑧 𝐽))
6564biimpar 502 . . . . . 6 ((𝜑𝑧 𝐽) → 𝑧X𝑘𝐶 (𝐹𝑘))
66 resixp 7888 . . . . . 6 ((𝐴𝐶𝑧X𝑘𝐶 (𝐹𝑘)) → (𝑧𝐴) ∈ X𝑘𝐴 (𝐹𝑘))
6763, 65, 66syl2anc 692 . . . . 5 ((𝜑𝑧 𝐽) → (𝑧𝐴) ∈ X𝑘𝐴 (𝐹𝑘))
6827adantr 481 . . . . 5 ((𝜑𝑧 𝐽) → X𝑘𝐴 (𝐹𝑘) = 𝑋)
6967, 68eleqtrd 2706 . . . 4 ((𝜑𝑧 𝐽) → (𝑧𝐴) ∈ 𝑋)
7043adantr 481 . . . . . 6 ((𝜑𝑧 𝐽) → 𝐵𝐶)
71 resixp 7888 . . . . . 6 ((𝐵𝐶𝑧X𝑘𝐶 (𝐹𝑘)) → (𝑧𝐵) ∈ X𝑘𝐵 (𝐹𝑘))
7270, 65, 71syl2anc 692 . . . . 5 ((𝜑𝑧 𝐽) → (𝑧𝐵) ∈ X𝑘𝐵 (𝐹𝑘))
7351adantr 481 . . . . 5 ((𝜑𝑧 𝐽) → X𝑘𝐵 (𝐹𝑘) = 𝑌)
7472, 73eleqtrd 2706 . . . 4 ((𝜑𝑧 𝐽) → (𝑧𝐵) ∈ 𝑌)
75 opelxpi 5113 . . . 4 (((𝑧𝐴) ∈ 𝑋 ∧ (𝑧𝐵) ∈ 𝑌) → ⟨(𝑧𝐴), (𝑧𝐵)⟩ ∈ (𝑋 × 𝑌))
7669, 74, 75syl2anc 692 . . 3 ((𝜑𝑧 𝐽) → ⟨(𝑧𝐴), (𝑧𝐵)⟩ ∈ (𝑋 × 𝑌))
77 eqop 7156 . . . . 5 (𝑤 ∈ (𝑋 × 𝑌) → (𝑤 = ⟨(𝑧𝐴), (𝑧𝐵)⟩ ↔ ((1st𝑤) = (𝑧𝐴) ∧ (2nd𝑤) = (𝑧𝐵))))
7877ad2antrl 763 . . . 4 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (𝑤 = ⟨(𝑧𝐴), (𝑧𝐵)⟩ ↔ ((1st𝑤) = (𝑧𝐴) ∧ (2nd𝑤) = (𝑧𝐵))))
7965adantrl 751 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → 𝑧X𝑘𝐶 (𝐹𝑘))
80 ixpfn 7859 . . . . . . . . 9 (𝑧X𝑘𝐶 (𝐹𝑘) → 𝑧 Fn 𝐶)
81 fnresdm 5960 . . . . . . . . 9 (𝑧 Fn 𝐶 → (𝑧𝐶) = 𝑧)
8279, 80, 813syl 18 . . . . . . . 8 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (𝑧𝐶) = 𝑧)
8317reseq2d 5360 . . . . . . . . 9 (𝜑 → (𝑧𝐶) = (𝑧 ↾ (𝐴𝐵)))
8483adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (𝑧𝐶) = (𝑧 ↾ (𝐴𝐵)))
8582, 84eqtr3d 2662 . . . . . . 7 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → 𝑧 = (𝑧 ↾ (𝐴𝐵)))
86 resundi 5373 . . . . . . 7 (𝑧 ↾ (𝐴𝐵)) = ((𝑧𝐴) ∪ (𝑧𝐵))
8785, 86syl6eq 2676 . . . . . 6 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → 𝑧 = ((𝑧𝐴) ∪ (𝑧𝐵)))
88 uneq12 3745 . . . . . . 7 (((1st𝑤) = (𝑧𝐴) ∧ (2nd𝑤) = (𝑧𝐵)) → ((1st𝑤) ∪ (2nd𝑤)) = ((𝑧𝐴) ∪ (𝑧𝐵)))
8988eqeq2d 2636 . . . . . 6 (((1st𝑤) = (𝑧𝐴) ∧ (2nd𝑤) = (𝑧𝐵)) → (𝑧 = ((1st𝑤) ∪ (2nd𝑤)) ↔ 𝑧 = ((𝑧𝐴) ∪ (𝑧𝐵))))
9087, 89syl5ibrcom 237 . . . . 5 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (((1st𝑤) = (𝑧𝐴) ∧ (2nd𝑤) = (𝑧𝐵)) → 𝑧 = ((1st𝑤) ∪ (2nd𝑤))))
91 ixpfn 7859 . . . . . . . . . . . 12 ((1st𝑤) ∈ X𝑘𝐴 (𝐹𝑘) → (1st𝑤) Fn 𝐴)
9229, 91syl 17 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → (1st𝑤) Fn 𝐴)
9392adantrr 752 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (1st𝑤) Fn 𝐴)
94 dffn2 6006 . . . . . . . . . 10 ((1st𝑤) Fn 𝐴 ↔ (1st𝑤):𝐴⟶V)
9593, 94sylib 208 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (1st𝑤):𝐴⟶V)
9651adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → X𝑘𝐵 (𝐹𝑘) = 𝑌)
9731, 96eleqtrrd 2707 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → (2nd𝑤) ∈ X𝑘𝐵 (𝐹𝑘))
98 ixpfn 7859 . . . . . . . . . . . 12 ((2nd𝑤) ∈ X𝑘𝐵 (𝐹𝑘) → (2nd𝑤) Fn 𝐵)
9997, 98syl 17 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝑋 × 𝑌)) → (2nd𝑤) Fn 𝐵)
10099adantrr 752 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (2nd𝑤) Fn 𝐵)
101 dffn2 6006 . . . . . . . . . 10 ((2nd𝑤) Fn 𝐵 ↔ (2nd𝑤):𝐵⟶V)
102100, 101sylib 208 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (2nd𝑤):𝐵⟶V)
103 res0 5364 . . . . . . . . . . 11 ((1st𝑤) ↾ ∅) = ∅
104 res0 5364 . . . . . . . . . . 11 ((2nd𝑤) ↾ ∅) = ∅
105103, 104eqtr4i 2651 . . . . . . . . . 10 ((1st𝑤) ↾ ∅) = ((2nd𝑤) ↾ ∅)
10633adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (𝐴𝐵) = ∅)
107106reseq2d 5360 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → ((1st𝑤) ↾ (𝐴𝐵)) = ((1st𝑤) ↾ ∅))
108106reseq2d 5360 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → ((2nd𝑤) ↾ (𝐴𝐵)) = ((2nd𝑤) ↾ ∅))
109105, 107, 1083eqtr4a 2686 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → ((1st𝑤) ↾ (𝐴𝐵)) = ((2nd𝑤) ↾ (𝐴𝐵)))
110 fresaunres1 6036 . . . . . . . . 9 (((1st𝑤):𝐴⟶V ∧ (2nd𝑤):𝐵⟶V ∧ ((1st𝑤) ↾ (𝐴𝐵)) = ((2nd𝑤) ↾ (𝐴𝐵))) → (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐴) = (1st𝑤))
11195, 102, 109, 110syl3anc 1323 . . . . . . . 8 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐴) = (1st𝑤))
112111eqcomd 2632 . . . . . . 7 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (1st𝑤) = (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐴))
113 fresaunres2 6035 . . . . . . . . 9 (((1st𝑤):𝐴⟶V ∧ (2nd𝑤):𝐵⟶V ∧ ((1st𝑤) ↾ (𝐴𝐵)) = ((2nd𝑤) ↾ (𝐴𝐵))) → (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐵) = (2nd𝑤))
11495, 102, 109, 113syl3anc 1323 . . . . . . . 8 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐵) = (2nd𝑤))
115114eqcomd 2632 . . . . . . 7 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (2nd𝑤) = (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐵))
116112, 115jca 554 . . . . . 6 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → ((1st𝑤) = (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐴) ∧ (2nd𝑤) = (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐵)))
117 reseq1 5354 . . . . . . . 8 (𝑧 = ((1st𝑤) ∪ (2nd𝑤)) → (𝑧𝐴) = (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐴))
118117eqeq2d 2636 . . . . . . 7 (𝑧 = ((1st𝑤) ∪ (2nd𝑤)) → ((1st𝑤) = (𝑧𝐴) ↔ (1st𝑤) = (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐴)))
119 reseq1 5354 . . . . . . . 8 (𝑧 = ((1st𝑤) ∪ (2nd𝑤)) → (𝑧𝐵) = (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐵))
120119eqeq2d 2636 . . . . . . 7 (𝑧 = ((1st𝑤) ∪ (2nd𝑤)) → ((2nd𝑤) = (𝑧𝐵) ↔ (2nd𝑤) = (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐵)))
121118, 120anbi12d 746 . . . . . 6 (𝑧 = ((1st𝑤) ∪ (2nd𝑤)) → (((1st𝑤) = (𝑧𝐴) ∧ (2nd𝑤) = (𝑧𝐵)) ↔ ((1st𝑤) = (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐴) ∧ (2nd𝑤) = (((1st𝑤) ∪ (2nd𝑤)) ↾ 𝐵))))
122116, 121syl5ibrcom 237 . . . . 5 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (𝑧 = ((1st𝑤) ∪ (2nd𝑤)) → ((1st𝑤) = (𝑧𝐴) ∧ (2nd𝑤) = (𝑧𝐵))))
12390, 122impbid 202 . . . 4 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (((1st𝑤) = (𝑧𝐴) ∧ (2nd𝑤) = (𝑧𝐵)) ↔ 𝑧 = ((1st𝑤) ∪ (2nd𝑤))))
12478, 123bitrd 268 . . 3 ((𝜑 ∧ (𝑤 ∈ (𝑋 × 𝑌) ∧ 𝑧 𝐽)) → (𝑤 = ⟨(𝑧𝐴), (𝑧𝐵)⟩ ↔ 𝑧 = ((1st𝑤) ∪ (2nd𝑤))))
1258, 62, 76, 124f1ocnv2d 6840 . 2 (𝜑 → (𝐺:(𝑋 × 𝑌)–1-1-onto 𝐽𝐺 = (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩)))
126125simprd 479 1 (𝜑𝐺 = (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1992  Vcvv 3191  cdif 3557  cun 3558  cin 3559  wss 3560  c0 3896  cop 4159   cuni 4407  cmpt 4678   × cxp 5077  ccnv 5078  cres 5081   Fn wfn 5845  wf 5846  1-1-ontowf1o 5849  cfv 5850  cmpt2 6607  1st c1st 7114  2nd c2nd 7115  Xcixp 7853  tcpt 16015  Topctop 20612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-oadd 7510  df-er 7688  df-ixp 7854  df-en 7901  df-fin 7904  df-fi 8262  df-topgen 16020  df-pt 16021  df-top 20616  df-bases 20617
This theorem is referenced by:  ptunhmeo  21516
  Copyright terms: Public domain W3C validator