Theorem uniss 2525

Description: Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.

Assertion

Ref	Expression
uniss	⊢ (A ⊆ B → ∪A ⊆ ∪B)

Proof of Theorem uniss

Step	Hyp	Ref	Expression
1		ssel 2066	. . . . . 6 ⊢ (A ⊆ B → (y ∈ A → y ∈ B))
2	1	anim2d 563	. . . . 5 ⊢ (A ⊆ B → ((x ∈ y ⋀ y ∈ A) → (x ∈ y ⋀ y ∈ B)))
3	2	19.22dv 1292	. . . 4 ⊢ (A ⊆ B → (∃y(x ∈ y ⋀ y ∈ A) → ∃y(x ∈ y ⋀ y ∈ B)))
4	3	19.21aiv 1288	. . 3 ⊢ (A ⊆ B → ∀x(∃y(x ∈ y ⋀ y ∈ A) → ∃y(x ∈ y ⋀ y ∈ B)))
5		ss2ab 2119	. . 3 ⊢ ({x∣∃y(x ∈ y ⋀ y ∈ A)} ⊆ {x∣∃y(x ∈ y ⋀ y ∈ B)} ↔ ∀x(∃y(x ∈ y ⋀ y ∈ A) → ∃y(x ∈ y ⋀ y ∈ B)))
6	4, 5	sylibr 200	. 2 ⊢ (A ⊆ B → {x∣∃y(x ∈ y ⋀ y ∈ A)} ⊆ {x∣∃y(x ∈ y ⋀ y ∈ B)})
7		df-uni 2508	. 2 ⊢ ∪A = {x∣∃y(x ∈ y ⋀ y ∈ A)}
8		df-uni 2508	. 2 ⊢ ∪B = {x∣∃y(x ∈ y ⋀ y ∈ B)}
9	6, 7, 8	3sstr4g 2105	1 ⊢ (A ⊆ B → ∪A ⊆ ∪B)

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 956   ∈ wcel 960  ∃wex 982  {cab 1466   ⊆ wss 2050  ∪cuni 2507

This theorem is referenced by:  unidif 2534  intssuni2 2560  sspwuni 2764  unixpss 3264  relfld 3521  unixp0 3524  trcl 4655  rankuni 4708  cflim 4921  unirnioo 6403  tgval2t 7616  unitgt 7622  tgclt 7623  tgsst 7635  basgen2t 7638  distop 7646  fctopOLD 7647  cctop 7649  cncnplem1 7771  uniopn 7858  opnuni 7865  unirnbl 7872  dfchsup2 9293  hsupval2t 9295  hsupvalt 9296  shsupclt 9301  hsupss 9304  shsupunss 9310  shatomistic 10283  inposet 10477  fgsb 10555

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056  df-uni 2508

Copyright terms: Public domain