Nuprl - Proof: fun-graph-rel-graph 3

(14steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: fun-graph-rel-graph 3

1. A: Type
2. B: Type
3. f: ABA
4. a:A, b1,b2:B. f(a,b1) = f(a,b2) b1 = b2
5. a,a':A. Dec(b:B. a' = f(a,b))

Bij(AB; {p:(AA)| b:B. 2of(p) = f(1of(p),b) A }; p. < 1of(p),f(1of(p),2of(p)) > )

By: Unfold `biject` 0 THEN Unfolds [`inject`;`surject`] 0 THEN Reduce 0 THEN Try (Analyze THEN (Reduce 0) THEN Obvious)

Generated subgoals:

1 6. a1: AB
7. a2: AB
8. < 1of(a1),f(1of(a1),2of(a1)) > = < 1of(a2),f(1of(a2),2of(a2)) > {p:(AA)| b:B. 2of(p) = f(1of(p),b) A }
a1 = a2 4 steps

2 6. b: {p:(AA)| b:B. 2of(p) = f(1of(p),b) A }
a:(AB). < 1of(a),f(1of(a),2of(a)) > = b {p:(AA)| b:B. 2of(p) = f(1of(p),b) A } 5 steps

About:

(14steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc