Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  txss12 GIF version

Theorem txss12 12472
 Description: Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015.)
Assertion
Ref Expression
txss12 (((𝐵𝑉𝐷𝑊) ∧ (𝐴𝐵𝐶𝐷)) → (𝐴 ×t 𝐶) ⊆ (𝐵 ×t 𝐷))

Proof of Theorem txss12
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2140 . . . 4 ran (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦)) = ran (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦))
21txbasex 12463 . . 3 ((𝐵𝑉𝐷𝑊) → ran (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦)) ∈ V)
3 resmpo 5876 . . . . . 6 ((𝐴𝐵𝐶𝐷) → ((𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦)) ↾ (𝐴 × 𝐶)) = (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦)))
4 resss 4850 . . . . . 6 ((𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦)) ↾ (𝐴 × 𝐶)) ⊆ (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦))
53, 4eqsstrrdi 3154 . . . . 5 ((𝐴𝐵𝐶𝐷) → (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦)) ⊆ (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦)))
65adantl 275 . . . 4 (((𝐵𝑉𝐷𝑊) ∧ (𝐴𝐵𝐶𝐷)) → (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦)) ⊆ (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦)))
7 rnss 4776 . . . 4 ((𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦)) ⊆ (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦)) → ran (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦)) ⊆ ran (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦)))
86, 7syl 14 . . 3 (((𝐵𝑉𝐷𝑊) ∧ (𝐴𝐵𝐶𝐷)) → ran (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦)) ⊆ ran (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦)))
9 tgss 12269 . . 3 ((ran (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦)) ∈ V ∧ ran (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦)) ⊆ ran (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦))) → (topGen‘ran (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦))) ⊆ (topGen‘ran (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦))))
102, 8, 9syl2an2r 585 . 2 (((𝐵𝑉𝐷𝑊) ∧ (𝐴𝐵𝐶𝐷)) → (topGen‘ran (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦))) ⊆ (topGen‘ran (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦))))
11 ssexg 4074 . . . . 5 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
12 ssexg 4074 . . . . 5 ((𝐶𝐷𝐷𝑊) → 𝐶 ∈ V)
13 eqid 2140 . . . . . 6 ran (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦)) = ran (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦))
1413txval 12461 . . . . 5 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ×t 𝐶) = (topGen‘ran (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦))))
1511, 12, 14syl2an 287 . . . 4 (((𝐴𝐵𝐵𝑉) ∧ (𝐶𝐷𝐷𝑊)) → (𝐴 ×t 𝐶) = (topGen‘ran (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦))))
1615an4s 578 . . 3 (((𝐴𝐵𝐶𝐷) ∧ (𝐵𝑉𝐷𝑊)) → (𝐴 ×t 𝐶) = (topGen‘ran (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦))))
1716ancoms 266 . 2 (((𝐵𝑉𝐷𝑊) ∧ (𝐴𝐵𝐶𝐷)) → (𝐴 ×t 𝐶) = (topGen‘ran (𝑥𝐴, 𝑦𝐶 ↦ (𝑥 × 𝑦))))
181txval 12461 . . 3 ((𝐵𝑉𝐷𝑊) → (𝐵 ×t 𝐷) = (topGen‘ran (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦))))
1918adantr 274 . 2 (((𝐵𝑉𝐷𝑊) ∧ (𝐴𝐵𝐶𝐷)) → (𝐵 ×t 𝐷) = (topGen‘ran (𝑥𝐵, 𝑦𝐷 ↦ (𝑥 × 𝑦))))
2010, 17, 193sstr4d 3146 1 (((𝐵𝑉𝐷𝑊) ∧ (𝐴𝐵𝐶𝐷)) → (𝐴 ×t 𝐶) ⊆ (𝐵 ×t 𝐷))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332   ∈ wcel 1481  Vcvv 2689   ⊆ wss 3075   × cxp 4544  ran crn 4547   ↾ cres 4548  ‘cfv 5130  (class class class)co 5781   ∈ cmpo 5783  topGenctg 12172   ×t ctx 12458 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4050  ax-sep 4053  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-id 4222  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-ov 5784  df-oprab 5785  df-mpo 5786  df-1st 6045  df-2nd 6046  df-topgen 12178  df-tx 12459 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator