Metamath Proof Explorer

Theorem mptbi12f

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

Ref Expression
Hypotheses mptbi12f.1 ⊢Ⅎ_xA
mptbi12f.2 ⊢Ⅎ_xB
Assertion mptbi12f ⊢A=B∧∀x∈AD=E→x∈A⟼D=x∈B⟼E

Proof

Step Hyp Ref Expression
1 mptbi12f.1 ⊢Ⅎ_xA
2 mptbi12f.2 ⊢Ⅎ_xB
3 1 2 nfeq ⊢ℲxA=B
4 eleq2 ⊢A=B→x∈A↔x∈B
5 3 4 alrimi ⊢A=B→∀xx∈A↔x∈B
6 ax-5 ⊢x∈A↔x∈B→∀yx∈A↔x∈B
7 5 6 sylg ⊢A=B→∀x∀yx∈A↔x∈B
8 eqeq2 ⊢D=E→y=D↔y=E
9 8 alrimiv ⊢D=E→∀yy=D↔y=E
10 9 ralimi ⊢∀x∈AD=E→∀x∈A∀yy=D↔y=E
11 df-ral ⊢∀x∈A∀yy=D↔y=E↔∀xx∈A→∀yy=D↔y=E
12 10 11 sylib ⊢∀x∈AD=E→∀xx∈A→∀yy=D↔y=E
13 19.21v ⊢∀yx∈A→y=D↔y=E↔x∈A→∀yy=D↔y=E
14 13 albii ⊢∀x∀yx∈A→y=D↔y=E↔∀xx∈A→∀yy=D↔y=E
15 12 14 sylibr ⊢∀x∈AD=E→∀x∀yx∈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 ⊢∀yx∈A↔x∈B∧∀yx∈A→y=D↔y=E→∀yx∈A↔x∈B∧x∈A→y=D↔y=E
18 17 alanimi ⊢∀x∀yx∈A↔x∈B∧∀x∀yx∈A→y=D↔y=E→∀x∀yx∈A↔x∈B∧x∈A→y=D↔y=E
19 7 15 18 syl2an ⊢A=B∧∀x∈AD=E→∀x∀yx∈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∀yx∈A↔x∈B∧x∈A→y=D↔y=E→∀x∀yx∈A∧y=D↔x∈B∧y=E
99 19 98 syl ⊢A=B∧∀x∈AD=E→∀x∀yx∈A∧y=D↔x∈B∧y=E
100 eqopab2bw ⊢xy|x∈A∧y=D=xy|x∈B∧y=E↔∀x∀yx∈A∧y=D↔x∈B∧y=E
101 99 100 sylibr ⊢A=B∧∀x∈AD=E→xy|x∈A∧y=D=xy|x∈B∧y=E
102 df-mpt ⊢x∈A⟼D=xy|x∈A∧y=D
103 df-mpt ⊢x∈B⟼E=xy|x∈B∧y=E
104 101 102 103 3eqtr4g ⊢A=B∧∀x∈AD=E→x∈A⟼D=x∈B⟼E