ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exmidapne GIF version

Theorem exmidapne 7258
Description: Excluded middle implies there is only one tight apartness on any class, namely negated equality. (Contributed by Jim Kingdon, 14-Feb-2025.)
Assertion
Ref Expression
exmidapne (EXMID → (𝑅 TAp 𝐴𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}))
Distinct variable group:   𝑢,𝐴,𝑣
Allowed substitution hints:   𝑅(𝑣,𝑢)

Proof of Theorem exmidapne
Dummy variables 𝑝 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 528 . . . . . . 7 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → 𝑅 TAp 𝐴)
2 simpr 110 . . . . . . 7 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → 𝑝𝑅)
3 dftap2 7249 . . . . . . . . . 10 (𝑅 TAp 𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)) ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦))))
43biimpi 120 . . . . . . . . 9 (𝑅 TAp 𝐴 → (𝑅 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)) ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦))))
54simp1d 1009 . . . . . . . 8 (𝑅 TAp 𝐴𝑅 ⊆ (𝐴 × 𝐴))
65sseld 3154 . . . . . . 7 (𝑅 TAp 𝐴 → (𝑝𝑅𝑝 ∈ (𝐴 × 𝐴)))
71, 2, 6sylc 62 . . . . . 6 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → 𝑝 ∈ (𝐴 × 𝐴))
8 1st2nd2 6175 . . . . . 6 (𝑝 ∈ (𝐴 × 𝐴) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
97, 8syl 14 . . . . 5 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
10 xp1st 6165 . . . . . . . 8 (𝑝 ∈ (𝐴 × 𝐴) → (1st𝑝) ∈ 𝐴)
117, 10syl 14 . . . . . . 7 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → (1st𝑝) ∈ 𝐴)
12 xp2nd 6166 . . . . . . . 8 (𝑝 ∈ (𝐴 × 𝐴) → (2nd𝑝) ∈ 𝐴)
137, 12syl 14 . . . . . . 7 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → (2nd𝑝) ∈ 𝐴)
149, 2eqeltrrd 2255 . . . . . . . . . 10 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → ⟨(1st𝑝), (2nd𝑝)⟩ ∈ 𝑅)
1514adantr 276 . . . . . . . . 9 ((((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) ∧ (1st𝑝) = (2nd𝑝)) → ⟨(1st𝑝), (2nd𝑝)⟩ ∈ 𝑅)
16 simpr 110 . . . . . . . . . . 11 ((((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) ∧ (1st𝑝) = (2nd𝑝)) → (1st𝑝) = (2nd𝑝))
1716opeq2d 3785 . . . . . . . . . 10 ((((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) ∧ (1st𝑝) = (2nd𝑝)) → ⟨(1st𝑝), (1st𝑝)⟩ = ⟨(1st𝑝), (2nd𝑝)⟩)
18 id 19 . . . . . . . . . . . . . 14 (𝑥 = (1st𝑝) → 𝑥 = (1st𝑝))
1918, 18breq12d 4016 . . . . . . . . . . . . 13 (𝑥 = (1st𝑝) → (𝑥𝑅𝑥 ↔ (1st𝑝)𝑅(1st𝑝)))
2019notbid 667 . . . . . . . . . . . 12 (𝑥 = (1st𝑝) → (¬ 𝑥𝑅𝑥 ↔ ¬ (1st𝑝)𝑅(1st𝑝)))
214simp2d 1010 . . . . . . . . . . . . . 14 (𝑅 TAp 𝐴 → (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑥)))
2221simpld 112 . . . . . . . . . . . . 13 (𝑅 TAp 𝐴 → ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
2322ad3antlr 493 . . . . . . . . . . . 12 ((((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) ∧ (1st𝑝) = (2nd𝑝)) → ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
2411adantr 276 . . . . . . . . . . . 12 ((((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) ∧ (1st𝑝) = (2nd𝑝)) → (1st𝑝) ∈ 𝐴)
2520, 23, 24rspcdva 2846 . . . . . . . . . . 11 ((((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) ∧ (1st𝑝) = (2nd𝑝)) → ¬ (1st𝑝)𝑅(1st𝑝))
26 df-br 4004 . . . . . . . . . . 11 ((1st𝑝)𝑅(1st𝑝) ↔ ⟨(1st𝑝), (1st𝑝)⟩ ∈ 𝑅)
2725, 26sylnib 676 . . . . . . . . . 10 ((((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) ∧ (1st𝑝) = (2nd𝑝)) → ¬ ⟨(1st𝑝), (1st𝑝)⟩ ∈ 𝑅)
2817, 27eqneltrrd 2274 . . . . . . . . 9 ((((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) ∧ (1st𝑝) = (2nd𝑝)) → ¬ ⟨(1st𝑝), (2nd𝑝)⟩ ∈ 𝑅)
2915, 28pm2.65da 661 . . . . . . . 8 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → ¬ (1st𝑝) = (2nd𝑝))
3029neqned 2354 . . . . . . 7 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → (1st𝑝) ≠ (2nd𝑝))
3111, 13, 30jca31 309 . . . . . 6 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → (((1st𝑝) ∈ 𝐴 ∧ (2nd𝑝) ∈ 𝐴) ∧ (1st𝑝) ≠ (2nd𝑝)))
32 eleq1 2240 . . . . . . . . . 10 (𝑢 = (1st𝑝) → (𝑢𝐴 ↔ (1st𝑝) ∈ 𝐴))
33 eleq1 2240 . . . . . . . . . 10 (𝑣 = (2nd𝑝) → (𝑣𝐴 ↔ (2nd𝑝) ∈ 𝐴))
3432, 33bi2anan9 606 . . . . . . . . 9 ((𝑢 = (1st𝑝) ∧ 𝑣 = (2nd𝑝)) → ((𝑢𝐴𝑣𝐴) ↔ ((1st𝑝) ∈ 𝐴 ∧ (2nd𝑝) ∈ 𝐴)))
35 simpl 109 . . . . . . . . . 10 ((𝑢 = (1st𝑝) ∧ 𝑣 = (2nd𝑝)) → 𝑢 = (1st𝑝))
36 simpr 110 . . . . . . . . . 10 ((𝑢 = (1st𝑝) ∧ 𝑣 = (2nd𝑝)) → 𝑣 = (2nd𝑝))
3735, 36neeq12d 2367 . . . . . . . . 9 ((𝑢 = (1st𝑝) ∧ 𝑣 = (2nd𝑝)) → (𝑢𝑣 ↔ (1st𝑝) ≠ (2nd𝑝)))
3834, 37anbi12d 473 . . . . . . . 8 ((𝑢 = (1st𝑝) ∧ 𝑣 = (2nd𝑝)) → (((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣) ↔ (((1st𝑝) ∈ 𝐴 ∧ (2nd𝑝) ∈ 𝐴) ∧ (1st𝑝) ≠ (2nd𝑝))))
3938opelopabga 4263 . . . . . . 7 (((1st𝑝) ∈ 𝐴 ∧ (2nd𝑝) ∈ 𝐴) → (⟨(1st𝑝), (2nd𝑝)⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} ↔ (((1st𝑝) ∈ 𝐴 ∧ (2nd𝑝) ∈ 𝐴) ∧ (1st𝑝) ≠ (2nd𝑝))))
4011, 13, 39syl2anc 411 . . . . . 6 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → (⟨(1st𝑝), (2nd𝑝)⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} ↔ (((1st𝑝) ∈ 𝐴 ∧ (2nd𝑝) ∈ 𝐴) ∧ (1st𝑝) ≠ (2nd𝑝))))
4131, 40mpbird 167 . . . . 5 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → ⟨(1st𝑝), (2nd𝑝)⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)})
429, 41eqeltrd 2254 . . . 4 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝𝑅) → 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)})
43 relopab 4753 . . . . . . 7 Rel {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}
44 1st2nd 6181 . . . . . . 7 ((Rel {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
4543, 44mpan 424 . . . . . 6 (𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
4645adantl 277 . . . . 5 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
47 breq2 4007 . . . . . . . . . 10 (𝑦 = (2nd𝑝) → ((1st𝑝)𝑅𝑦 ↔ (1st𝑝)𝑅(2nd𝑝)))
4847notbid 667 . . . . . . . . 9 (𝑦 = (2nd𝑝) → (¬ (1st𝑝)𝑅𝑦 ↔ ¬ (1st𝑝)𝑅(2nd𝑝)))
49 eqeq2 2187 . . . . . . . . 9 (𝑦 = (2nd𝑝) → ((1st𝑝) = 𝑦 ↔ (1st𝑝) = (2nd𝑝)))
5048, 49imbi12d 234 . . . . . . . 8 (𝑦 = (2nd𝑝) → ((¬ (1st𝑝)𝑅𝑦 → (1st𝑝) = 𝑦) ↔ (¬ (1st𝑝)𝑅(2nd𝑝) → (1st𝑝) = (2nd𝑝))))
51 breq1 4006 . . . . . . . . . . . 12 (𝑥 = (1st𝑝) → (𝑥𝑅𝑦 ↔ (1st𝑝)𝑅𝑦))
5251notbid 667 . . . . . . . . . . 11 (𝑥 = (1st𝑝) → (¬ 𝑥𝑅𝑦 ↔ ¬ (1st𝑝)𝑅𝑦))
53 eqeq1 2184 . . . . . . . . . . 11 (𝑥 = (1st𝑝) → (𝑥 = 𝑦 ↔ (1st𝑝) = 𝑦))
5452, 53imbi12d 234 . . . . . . . . . 10 (𝑥 = (1st𝑝) → ((¬ 𝑥𝑅𝑦𝑥 = 𝑦) ↔ (¬ (1st𝑝)𝑅𝑦 → (1st𝑝) = 𝑦)))
5554ralbidv 2477 . . . . . . . . 9 (𝑥 = (1st𝑝) → (∀𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦) ↔ ∀𝑦𝐴 (¬ (1st𝑝)𝑅𝑦 → (1st𝑝) = 𝑦)))
564simp3d 1011 . . . . . . . . . . 11 (𝑅 TAp 𝐴 → (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)) ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦)))
5756simprd 114 . . . . . . . . . 10 (𝑅 TAp 𝐴 → ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦))
5857ad2antlr 489 . . . . . . . . 9 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦))
5932anbi1d 465 . . . . . . . . . . . . . 14 (𝑢 = (1st𝑝) → ((𝑢𝐴𝑣𝐴) ↔ ((1st𝑝) ∈ 𝐴𝑣𝐴)))
60 neeq1 2360 . . . . . . . . . . . . . 14 (𝑢 = (1st𝑝) → (𝑢𝑣 ↔ (1st𝑝) ≠ 𝑣))
6159, 60anbi12d 473 . . . . . . . . . . . . 13 (𝑢 = (1st𝑝) → (((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣) ↔ (((1st𝑝) ∈ 𝐴𝑣𝐴) ∧ (1st𝑝) ≠ 𝑣)))
6233anbi2d 464 . . . . . . . . . . . . . 14 (𝑣 = (2nd𝑝) → (((1st𝑝) ∈ 𝐴𝑣𝐴) ↔ ((1st𝑝) ∈ 𝐴 ∧ (2nd𝑝) ∈ 𝐴)))
63 neeq2 2361 . . . . . . . . . . . . . 14 (𝑣 = (2nd𝑝) → ((1st𝑝) ≠ 𝑣 ↔ (1st𝑝) ≠ (2nd𝑝)))
6462, 63anbi12d 473 . . . . . . . . . . . . 13 (𝑣 = (2nd𝑝) → ((((1st𝑝) ∈ 𝐴𝑣𝐴) ∧ (1st𝑝) ≠ 𝑣) ↔ (((1st𝑝) ∈ 𝐴 ∧ (2nd𝑝) ∈ 𝐴) ∧ (1st𝑝) ≠ (2nd𝑝))))
6561, 64elopabi 6195 . . . . . . . . . . . 12 (𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} → (((1st𝑝) ∈ 𝐴 ∧ (2nd𝑝) ∈ 𝐴) ∧ (1st𝑝) ≠ (2nd𝑝)))
6665adantl 277 . . . . . . . . . . 11 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → (((1st𝑝) ∈ 𝐴 ∧ (2nd𝑝) ∈ 𝐴) ∧ (1st𝑝) ≠ (2nd𝑝)))
6766simpld 112 . . . . . . . . . 10 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → ((1st𝑝) ∈ 𝐴 ∧ (2nd𝑝) ∈ 𝐴))
6867simpld 112 . . . . . . . . 9 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → (1st𝑝) ∈ 𝐴)
6955, 58, 68rspcdva 2846 . . . . . . . 8 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → ∀𝑦𝐴 (¬ (1st𝑝)𝑅𝑦 → (1st𝑝) = 𝑦))
7067simprd 114 . . . . . . . 8 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → (2nd𝑝) ∈ 𝐴)
7150, 69, 70rspcdva 2846 . . . . . . 7 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → (¬ (1st𝑝)𝑅(2nd𝑝) → (1st𝑝) = (2nd𝑝)))
7266simprd 114 . . . . . . . 8 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → (1st𝑝) ≠ (2nd𝑝))
7372neneqd 2368 . . . . . . 7 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → ¬ (1st𝑝) = (2nd𝑝))
74 exmidexmid 4196 . . . . . . . . 9 (EXMIDDECID (1st𝑝)𝑅(2nd𝑝))
75 con1dc 856 . . . . . . . . 9 (DECID (1st𝑝)𝑅(2nd𝑝) → ((¬ (1st𝑝)𝑅(2nd𝑝) → (1st𝑝) = (2nd𝑝)) → (¬ (1st𝑝) = (2nd𝑝) → (1st𝑝)𝑅(2nd𝑝))))
7674, 75syl 14 . . . . . . . 8 (EXMID → ((¬ (1st𝑝)𝑅(2nd𝑝) → (1st𝑝) = (2nd𝑝)) → (¬ (1st𝑝) = (2nd𝑝) → (1st𝑝)𝑅(2nd𝑝))))
7776ad2antrr 488 . . . . . . 7 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → ((¬ (1st𝑝)𝑅(2nd𝑝) → (1st𝑝) = (2nd𝑝)) → (¬ (1st𝑝) = (2nd𝑝) → (1st𝑝)𝑅(2nd𝑝))))
7871, 73, 77mp2d 47 . . . . . 6 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → (1st𝑝)𝑅(2nd𝑝))
79 df-br 4004 . . . . . 6 ((1st𝑝)𝑅(2nd𝑝) ↔ ⟨(1st𝑝), (2nd𝑝)⟩ ∈ 𝑅)
8078, 79sylib 122 . . . . 5 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → ⟨(1st𝑝), (2nd𝑝)⟩ ∈ 𝑅)
8146, 80eqeltrd 2254 . . . 4 (((EXMID𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → 𝑝𝑅)
8242, 81impbida 596 . . 3 ((EXMID𝑅 TAp 𝐴) → (𝑝𝑅𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}))
8382eqrdv 2175 . 2 ((EXMID𝑅 TAp 𝐴) → 𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)})
84 exmidexmid 4196 . . . . . . 7 (EXMIDDECID 𝑥 = 𝑦)
8584ralrimivw 2551 . . . . . 6 (EXMID → ∀𝑦𝐴 DECID 𝑥 = 𝑦)
8685ralrimivw 2551 . . . . 5 (EXMID → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
87 netap 7252 . . . . 5 (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} TAp 𝐴)
8886, 87syl 14 . . . 4 (EXMID → {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} TAp 𝐴)
8988adantr 276 . . 3 ((EXMID𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} TAp 𝐴)
90 tapeq1 7250 . . . 4 (𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} → (𝑅 TAp 𝐴 ↔ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} TAp 𝐴))
9190adantl 277 . . 3 ((EXMID𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → (𝑅 TAp 𝐴 ↔ {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} TAp 𝐴))
9289, 91mpbird 167 . 2 ((EXMID𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}) → 𝑅 TAp 𝐴)
9383, 92impbida 596 1 (EXMID → (𝑅 TAp 𝐴𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834  w3a 978   = wceq 1353  wcel 2148  wne 2347  wral 2455  wss 3129  cop 3595   class class class wbr 4003  {copab 4063  EXMIDwem 4194   × cxp 4624  Rel wrel 4631  cfv 5216  1st c1st 6138  2nd c2nd 6139   TAp wtap 7247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-mpt 4066  df-exmid 4195  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-fo 5222  df-fv 5224  df-1st 6140  df-2nd 6141  df-pap 7246  df-tap 7248
This theorem is referenced by:  exmidmotap  7259
  Copyright terms: Public domain W3C validator