Metamath Proof Explorer


Theorem ex-res

Description: Example for df-res . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion ex-res F = 2 6 3 9 B = 1 2 F B = 2 6

Proof

Step Hyp Ref Expression
1 simpl F = 2 6 3 9 B = 1 2 F = 2 6 3 9
2 df-pr 2 6 3 9 = 2 6 3 9
3 1 2 eqtrdi F = 2 6 3 9 B = 1 2 F = 2 6 3 9
4 3 reseq1d F = 2 6 3 9 B = 1 2 F B = 2 6 3 9 B
5 resundir 2 6 3 9 B = 2 6 B 3 9 B
6 4 5 eqtrdi F = 2 6 3 9 B = 1 2 F B = 2 6 B 3 9 B
7 2re 2
8 7 elexi 2 V
9 6re 6
10 9 elexi 6 V
11 8 10 relsnop Rel 2 6
12 dmsnopss dom 2 6 2
13 snsspr2 2 1 2
14 simpr F = 2 6 3 9 B = 1 2 B = 1 2
15 13 14 sseqtrrid F = 2 6 3 9 B = 1 2 2 B
16 12 15 sstrid F = 2 6 3 9 B = 1 2 dom 2 6 B
17 relssres Rel 2 6 dom 2 6 B 2 6 B = 2 6
18 11 16 17 sylancr F = 2 6 3 9 B = 1 2 2 6 B = 2 6
19 1re 1
20 1lt3 1 < 3
21 19 20 gtneii 3 1
22 2lt3 2 < 3
23 7 22 gtneii 3 2
24 21 23 nelpri ¬ 3 1 2
25 14 eleq2d F = 2 6 3 9 B = 1 2 3 B 3 1 2
26 24 25 mtbiri F = 2 6 3 9 B = 1 2 ¬ 3 B
27 ressnop0 ¬ 3 B 3 9 B =
28 26 27 syl F = 2 6 3 9 B = 1 2 3 9 B =
29 18 28 uneq12d F = 2 6 3 9 B = 1 2 2 6 B 3 9 B = 2 6
30 un0 2 6 = 2 6
31 29 30 eqtrdi F = 2 6 3 9 B = 1 2 2 6 B 3 9 B = 2 6
32 6 31 eqtrd F = 2 6 3 9 B = 1 2 F B = 2 6