Theorem ishgrag 16291

Description: Express the predicate "H is a hypergraph." Definition of hypergraph in [Diestel] p. 28, which states "A hypergraph is a pair (V, E) of disjoint sets, where the elements of E are non-empty subsets (of any cardinality) of V."

Because V and E are both used as symbols (for the universal class df-v 2294 and the epsilon relation df-eprel 3583, respectively) in Metamath, we instead use A to represent V, the set of vertices or atoms of the hypergraph, and B to represent E, the set of edges or blocks that each connect one or more atoms in A. (See Definition 2.1 in [McKMegPav] p. 2384 for an analogous use of atom and block in Greechie diagrams.)

Hypothesis

Ref	Expression
ishgrag.1	|- H = <.A, B>.

Assertion

Ref	Expression
ishgrag	|- ((A e. C /\ B e. D) -> (H e. HypGrph <-> ((A i^i B) = (/) /\ A.b e. B (b C_ A /\ b =/= (/)))))

Distinct variable groups:   A,b   B,b

Proof of Theorem ishgrag

Step	Hyp	Ref	Expression
1		ineq1 2789	. . . . . . 7 |- (x = A -> (x i^i y) = (A i^i y))
2	1	eqeq1d 1892	. . . . . 6 |- (x = A -> ((x i^i y) = (/) <-> (A i^i y) = (/)))
3		pweq 3036	. . . . . . . 8 |- (x = A -> ~Px = ~PA)
4	3	difeq1d 2725	. . . . . . 7 |- (x = A -> (~Px \ {(/)}) = (~PA \ {(/)}))
5	4	sseq2d 2645	. . . . . 6 |- (x = A -> (y C_ (~Px \ {(/)}) <-> y C_ (~PA \ {(/)})))
6	2, 5	anbi12d 690	. . . . 5 |- (x = A -> (((x i^i y) = (/) /\ y C_ (~Px \ {(/)})) <-> ((A i^i y) = (/) /\ y C_ (~PA \ {(/)}))))
7		ineq2 2790	. . . . . . 7 |- (y = B -> (A i^i y) = (A i^i B))
8	7	eqeq1d 1892	. . . . . 6 |- (y = B -> ((A i^i y) = (/) <-> (A i^i B) = (/)))
9		sseq1 2637	. . . . . 6 |- (y = B -> (y C_ (~PA \ {(/)}) <-> B C_ (~PA \ {(/)})))
10	8, 9	anbi12d 690	. . . . 5 |- (y = B -> (((A i^i y) = (/) /\ y C_ (~PA \ {(/)})) <-> ((A i^i B) = (/) /\ B C_ (~PA \ {(/)}))))
11	6, 10	opelopabg 3567	. . . 4 |- ((A e. C /\ B e. D) -> (<.A, B>. e. {<.x, y>. | ((x i^i y) = (/) /\ y C_ (~Px \ {(/)}))} <-> ((A i^i B) = (/) /\ B C_ (~PA \ {(/)}))))
12		df-hgra 16288	. . . . 5 |- HypGrph = {<.x, y>. | ((x i^i y) = (/) /\ y C_ (~Px \ {(/)}))}
13	12	eleq2i 1961	. . . 4 |- (<.A, B>. e. HypGrph <-> <.A, B>. e. {<.x, y>. | ((x i^i y) = (/) /\ y C_ (~Px \ {(/)}))})
14	11, 13	syl5bb 591	. . 3 |- ((A e. C /\ B e. D) -> (<.A, B>. e. HypGrph <-> ((A i^i B) = (/) /\ B C_ (~PA \ {(/)}))))
15		ishgrag.1	. . . 4 |- H = <.A, B>.
16	15	eleq1i 1960	. . 3 |- (H e. HypGrph <-> <.A, B>. e. HypGrph)
17	14, 16	syl5bb 591	. 2 |- ((A e. C /\ B e. D) -> (H e. HypGrph <-> ((A i^i B) = (/) /\ B C_ (~PA \ {(/)}))))
18		blkssatm 16289	. . 3 |- (B C_ (~PA \ {(/)}) <-> A.b e. B (b C_ A /\ b =/= (/)))
19	18	anbi2i 538	. 2 |- (((A i^i B) = (/) /\ B C_ (~PA \ {(/)})) <-> ((A i^i B) = (/) /\ A.b e. B (b C_ A /\ b =/= (/))))
20	17, 19	syl6bb 595	1 |- ((A e. C /\ B e. D) -> (H e. HypGrph <-> ((A i^i B) = (/) /\ A.b e. B (b C_ A /\ b =/= (/)))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105   \ cdif 2590   i^i cin 2592   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  {csn 3044  <.cop 3046  {copab 3395  HypGrphchgra 16287

This theorem is referenced by:  emhgrat 16297

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-opab 3396  df-hgra 16288

Copyright terms: Public domain