Metamath Proof Explorer

Theorem mptbi12f

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

Ref Expression
Hypotheses mptbi12f.1 ⊢ Ⅎ 𝑥 𝐴
mptbi12f.2 ⊢ Ⅎ 𝑥 𝐵
Assertion mptbi12f ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝐷 = 𝐸 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐸 ) )

Proof

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