Metamath Proof Explorer


Theorem mptbi12f

Description: Equality deduction for maps-to notations. (Contributed by Giovanni Mascellani, 10-Apr-2018)

Ref Expression
Hypotheses mptbi12f.1 _ x A
mptbi12f.2 _ x B
Assertion mptbi12f A = B x A D = E x A D = x B E

Proof

Step Hyp Ref Expression
1 mptbi12f.1 _ x A
2 mptbi12f.2 _ x B
3 1 2 nfeq x A = B
4 eleq2 A = B x A x B
5 3 4 alrimi A = B x x A x B
6 ax-5 x A x B y x A x B
7 5 6 sylg A = B x y x A x B
8 eqeq2 D = E y = D y = E
9 8 alrimiv D = E y y = D y = E
10 9 ralimi x A D = E x A y y = D y = E
11 df-ral x A y y = D y = E x x A y y = D y = E
12 10 11 sylib x A D = E x x A y y = D y = E
13 19.21v y x A y = D y = E x A y y = D y = E
14 13 albii x y x A y = D y = E x x A y y = D y = E
15 12 14 sylibr x A D = E x y x A y = D y = E
16 id x A x B x A y = D y = E x A x B x A y = D y = E
17 16 alanimi y x A x B y x A y = D y = E y x A x B x A y = D y = E
18 17 alanimi x y x A x B x y x A y = D y = E x y x A x B x A y = D y = E
19 7 15 18 syl2an A = B x A D = E x y x A x B x A y = D y = E
20 tsan2 ¬ x A x B x A y = D y = E x A y = D x B y = E x A ¬ x A y = D
21 20 ord ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A ¬ x A y = D
22 tsbi2 ¬ x A x B x A y = D y = E x A y = D x B y = E x A y = D x B y = E x A y = D x B y = E
23 22 ord ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A y = D x B y = E x A y = D x B y = E
24 23 a1dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A y = D x B y = E x A x B x A y = D y = E x A y = D x B y = E
25 ax-1 ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A y = D x B y = E ¬ x A x B x A y = D y = E x A y = D x B y = E
26 24 25 contrd ¬ x A x B x A y = D y = E x A y = D x B y = E x A y = D x B y = E
27 26 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A x A y = D x B y = E
28 21 27 cnf1dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A x B y = E
29 simplim ¬ x A x B x A y = D y = E x A y = D x B y = E x A x B x A y = D y = E
30 29 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A ¬ x B x A x B x A y = D y = E
31 tsbi3 ¬ x A x B x A y = D y = E x A y = D x B y = E x A ¬ x B ¬ x A x B
32 31 ord ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A ¬ x B ¬ x A x B
33 tsan2 ¬ x A x B x A y = D y = E x A y = D x B y = E x A x B ¬ x A x B x A y = D y = E
34 33 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A ¬ x B x A x B ¬ x A x B x A y = D y = E
35 32 34 cnf1dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A ¬ x B ¬ x A x B x A y = D y = E
36 30 35 contrd ¬ x A x B x A y = D y = E x A y = D x B y = E x A ¬ x B
37 36 ord ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A ¬ x B
38 tsan2 ¬ x A x B x A y = D y = E x A y = D x B y = E x B ¬ x B y = E
39 38 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A x B ¬ x B y = E
40 37 39 cnf1dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A ¬ x B y = E
41 28 40 contrd ¬ x A x B x A y = D y = E x A y = D x B y = E x A
42 41 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A
43 29 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A x B x A y = D y = E
44 tsan3 ¬ x A x B x A y = D y = E x A y = D x B y = E x A y = D y = E ¬ x A x B x A y = D y = E
45 44 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A y = D y = E ¬ x A x B x A y = D y = E
46 43 45 cnfn2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A y = D y = E
47 42 46 mpdd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ y = D y = E
48 notnotr ¬ ¬ x B y = E x B y = E
49 48 a1i ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E x B y = E
50 38 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E x B ¬ x B y = E
51 49 50 cnfn2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E x B
52 36 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E x A ¬ x B
53 51 52 cnfn2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E x A
54 tsan3 ¬ x A x B x A y = D y = E x A y = D x B y = E y = E ¬ x B y = E
55 54 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E y = E ¬ x B y = E
56 49 55 cnfn2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E y = E
57 29 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E x A x B x A y = D y = E
58 44 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E x A y = D y = E ¬ x A x B x A y = D y = E
59 57 58 cnfn2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E x A y = D y = E
60 53 59 mpdd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E y = D y = E
61 tsbi3 ¬ x A x B x A y = D y = E x A y = D x B y = E y = D ¬ y = E ¬ y = D y = E
62 61 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E y = D ¬ y = E ¬ y = D y = E
63 60 62 cnfn2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E y = D ¬ y = E
64 56 63 cnfn2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E y = D
65 53 64 jcad ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E x A y = D
66 ax-1 ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E ¬ x A x B x A y = D y = E x A y = D x B y = E
67 tsim3 ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A y = D x B y = E x A x B x A y = D y = E x A y = D x B y = E
68 67 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E ¬ x A y = D x B y = E x A x B x A y = D y = E x A y = D x B y = E
69 66 68 cnf2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E ¬ x A y = D x B y = E
70 tsbi1 ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A y = D ¬ x B y = E x A y = D x B y = E
71 70 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E ¬ x A y = D ¬ x B y = E x A y = D x B y = E
72 69 71 cnf2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E ¬ x A y = D ¬ x B y = E
73 49 72 cnfn2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E ¬ x A y = D
74 65 73 contrd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x B y = E
75 74 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B y = E
76 26 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A y = D x B y = E
77 75 76 cnf2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A y = D
78 tsan3 ¬ x A x B x A y = D y = E x A y = D x B y = E y = D ¬ x A y = D
79 78 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ y = D ¬ x A y = D
80 77 79 cnfn2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ y = D
81 33 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A x B ¬ x A x B x A y = D y = E
82 43 81 cnfn2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A x B
83 tsbi4 ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x A x B ¬ x A x B
84 83 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x A x B ¬ x A x B
85 82 84 cnfn2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x A x B
86 42 85 cnfn1dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x B
87 tsan1 ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ x B ¬ y = E x B y = E
88 87 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B ¬ y = E x B y = E
89 75 88 cnf2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ x B ¬ y = E
90 86 89 cnfn1dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ y = E
91 tsbi4 ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ y = D y = E ¬ y = D y = E
92 91 a1d ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ y = D y = E ¬ y = D y = E
93 92 or32dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ y = D ¬ y = D y = E y = E
94 90 93 cnf2dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ y = D ¬ y = D y = E
95 80 94 cnfn1dd ¬ x A x B x A y = D y = E x A y = D x B y = E ¬ ¬ y = D y = E
96 47 95 contrd ¬ x A x B x A y = D y = E x A y = D x B y = E
97 96 efald2 x A x B x A y = D y = E x A y = D x B y = E
98 97 2alimi x y x A x B x A y = D y = E x y x A y = D x B y = E
99 19 98 syl A = B x A D = E x y x A y = D x B y = E
100 eqopab2bw x y | x A y = D = x y | x B y = E x y x A y = D x B y = E
101 99 100 sylibr A = B x A D = E x y | x A y = D = x y | x B y = E
102 df-mpt x A D = x y | x A y = D
103 df-mpt x B E = x y | x B y = E
104 101 102 103 3eqtr4g A = B x A D = E x A D = x B E