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

Theorem fiuni 6859
Description: The union of the finite intersections of a set is simply the union of the set itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
Assertion
Ref Expression
fiuni  |-  ( A  e.  V  ->  U. A  =  U. ( fi `  A ) )

Proof of Theorem fiuni
Dummy variables  x  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssfii 6855 . . 3  |-  ( A  e.  V  ->  A  C_  ( fi `  A
) )
21unissd 3755 . 2  |-  ( A  e.  V  ->  U. A  C_ 
U. ( fi `  A ) )
3 eluni 3734 . . . . 5  |-  ( x  e.  U. ( fi
`  A )  <->  E. y
( x  e.  y  /\  y  e.  ( fi `  A ) ) )
43biimpi 119 . . . 4  |-  ( x  e.  U. ( fi
`  A )  ->  E. y ( x  e.  y  /\  y  e.  ( fi `  A
) ) )
54adantl 275 . . 3  |-  ( ( A  e.  V  /\  x  e.  U. ( fi `  A ) )  ->  E. y ( x  e.  y  /\  y  e.  ( fi `  A
) ) )
6 simprr 521 . . . . 5  |-  ( ( ( A  e.  V  /\  x  e.  U. ( fi `  A ) )  /\  ( x  e.  y  /\  y  e.  ( fi `  A
) ) )  -> 
y  e.  ( fi
`  A ) )
7 elfi2 6853 . . . . . 6  |-  ( A  e.  V  ->  (
y  e.  ( fi
`  A )  <->  E. z  e.  ( ( ~P A  i^i  Fin )  \  { (/)
} ) y  = 
|^| z ) )
87ad2antrr 479 . . . . 5  |-  ( ( ( A  e.  V  /\  x  e.  U. ( fi `  A ) )  /\  ( x  e.  y  /\  y  e.  ( fi `  A
) ) )  -> 
( y  e.  ( fi `  A )  <->  E. z  e.  (
( ~P A  i^i  Fin )  \  { (/) } ) y  =  |^| z ) )
96, 8mpbid 146 . . . 4  |-  ( ( ( A  e.  V  /\  x  e.  U. ( fi `  A ) )  /\  ( x  e.  y  /\  y  e.  ( fi `  A
) ) )  ->  E. z  e.  (
( ~P A  i^i  Fin )  \  { (/) } ) y  =  |^| z )
10 simprr 521 . . . . . 6  |-  ( ( ( ( A  e.  V  /\  x  e. 
U. ( fi `  A ) )  /\  ( x  e.  y  /\  y  e.  ( fi `  A ) ) )  /\  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  /\  y  =  |^| z ) )  ->  y  =  |^| z )
11 eldifi 3193 . . . . . . . . . 10  |-  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  -> 
z  e.  ( ~P A  i^i  Fin )
)
1211elin1d 3260 . . . . . . . . 9  |-  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  -> 
z  e.  ~P A
)
1312elpwid 3516 . . . . . . . 8  |-  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  -> 
z  C_  A )
1413ad2antrl 481 . . . . . . 7  |-  ( ( ( ( A  e.  V  /\  x  e. 
U. ( fi `  A ) )  /\  ( x  e.  y  /\  y  e.  ( fi `  A ) ) )  /\  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  /\  y  =  |^| z ) )  ->  z  C_  A )
15 eldifsni 3647 . . . . . . . . 9  |-  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  -> 
z  =/=  (/) )
1611elin2d 3261 . . . . . . . . . 10  |-  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  -> 
z  e.  Fin )
17 fin0 6772 . . . . . . . . . 10  |-  ( z  e.  Fin  ->  (
z  =/=  (/)  <->  E. w  w  e.  z )
)
1816, 17syl 14 . . . . . . . . 9  |-  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  -> 
( z  =/=  (/)  <->  E. w  w  e.  z )
)
1915, 18mpbid 146 . . . . . . . 8  |-  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  ->  E. w  w  e.  z )
2019ad2antrl 481 . . . . . . 7  |-  ( ( ( ( A  e.  V  /\  x  e. 
U. ( fi `  A ) )  /\  ( x  e.  y  /\  y  e.  ( fi `  A ) ) )  /\  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  /\  y  =  |^| z ) )  ->  E. w  w  e.  z )
21 intssuni2m 3790 . . . . . . 7  |-  ( ( z  C_  A  /\  E. w  w  e.  z )  ->  |^| z  C_  U. A )
2214, 20, 21syl2anc 408 . . . . . 6  |-  ( ( ( ( A  e.  V  /\  x  e. 
U. ( fi `  A ) )  /\  ( x  e.  y  /\  y  e.  ( fi `  A ) ) )  /\  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  /\  y  =  |^| z ) )  ->  |^| z  C_  U. A )
2310, 22eqsstrd 3128 . . . . 5  |-  ( ( ( ( A  e.  V  /\  x  e. 
U. ( fi `  A ) )  /\  ( x  e.  y  /\  y  e.  ( fi `  A ) ) )  /\  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  /\  y  =  |^| z ) )  ->  y  C_  U. A )
24 simplrl 524 . . . . 5  |-  ( ( ( ( A  e.  V  /\  x  e. 
U. ( fi `  A ) )  /\  ( x  e.  y  /\  y  e.  ( fi `  A ) ) )  /\  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  /\  y  =  |^| z ) )  ->  x  e.  y )
2523, 24sseldd 3093 . . . 4  |-  ( ( ( ( A  e.  V  /\  x  e. 
U. ( fi `  A ) )  /\  ( x  e.  y  /\  y  e.  ( fi `  A ) ) )  /\  ( z  e.  ( ( ~P A  i^i  Fin )  \  { (/) } )  /\  y  =  |^| z ) )  ->  x  e.  U. A )
269, 25rexlimddv 2552 . . 3  |-  ( ( ( A  e.  V  /\  x  e.  U. ( fi `  A ) )  /\  ( x  e.  y  /\  y  e.  ( fi `  A
) ) )  ->  x  e.  U. A )
275, 26exlimddv 1870 . 2  |-  ( ( A  e.  V  /\  x  e.  U. ( fi `  A ) )  ->  x  e.  U. A )
282, 27eqelssd 3111 1  |-  ( A  e.  V  ->  U. A  =  U. ( fi `  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1331   E.wex 1468    e. wcel 1480    =/= wne 2306   E.wrex 2415    \ cdif 3063    i^i cin 3065    C_ wss 3066   (/)c0 3358   ~Pcpw 3505   {csn 3522   U.cuni 3731   |^|cint 3766   ` cfv 5118   Fincfn 6627   ficfi 6849
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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-nul 4049  ax-pow 4093  ax-pr 4126  ax-un 4350  ax-iinf 4497
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-ral 2419  df-rex 2420  df-v 2683  df-sbc 2905  df-csb 2999  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-int 3767  df-br 3925  df-opab 3985  df-mpt 3986  df-id 4210  df-suc 4288  df-iom 4500  df-xp 4540  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-rn 4545  df-res 4546  df-ima 4547  df-iota 5083  df-fun 5120  df-fn 5121  df-f 5122  df-f1 5123  df-fo 5124  df-f1o 5125  df-fv 5126  df-1o 6306  df-er 6422  df-en 6628  df-fin 6630  df-fi 6850
This theorem is referenced by:  fipwssg  6860
  Copyright terms: Public domain W3C validator