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

Theorem 2omotaplemap 7256
Description: Lemma for 2omotap 7258. (Contributed by Jim Kingdon, 6-Feb-2025.)
Assertion
Ref Expression
2omotaplemap (¬ ¬ 𝜑 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} TAp 2o)
Distinct variable group:   𝜑,𝑢,𝑣

Proof of Theorem 2omotaplemap
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opabssxp 4701 . . 3 {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ⊆ (2o × 2o)
21a1i 9 . 2 (¬ ¬ 𝜑 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ⊆ (2o × 2o))
3 df-br 4005 . . . . . . . 8 (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))})
4 neeq1 2360 . . . . . . . . . 10 (𝑢 = 𝑎 → (𝑢𝑣𝑎𝑣))
54anbi2d 464 . . . . . . . . 9 (𝑢 = 𝑎 → ((𝜑𝑢𝑣) ↔ (𝜑𝑎𝑣)))
6 neeq2 2361 . . . . . . . . . 10 (𝑣 = 𝑏 → (𝑎𝑣𝑎𝑏))
76anbi2d 464 . . . . . . . . 9 (𝑣 = 𝑏 → ((𝜑𝑎𝑣) ↔ (𝜑𝑎𝑏)))
85, 7opelopab2 4271 . . . . . . . 8 ((𝑎 ∈ 2o𝑏 ∈ 2o) → (⟨𝑎, 𝑏⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ↔ (𝜑𝑎𝑏)))
93, 8bitrid 192 . . . . . . 7 ((𝑎 ∈ 2o𝑏 ∈ 2o) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏 ↔ (𝜑𝑎𝑏)))
10 df-br 4005 . . . . . . . 8 (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎 ↔ ⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))})
11 neeq1 2360 . . . . . . . . . . . 12 (𝑢 = 𝑏 → (𝑢𝑣𝑏𝑣))
1211anbi2d 464 . . . . . . . . . . 11 (𝑢 = 𝑏 → ((𝜑𝑢𝑣) ↔ (𝜑𝑏𝑣)))
13 neeq2 2361 . . . . . . . . . . . 12 (𝑣 = 𝑎 → (𝑏𝑣𝑏𝑎))
1413anbi2d 464 . . . . . . . . . . 11 (𝑣 = 𝑎 → ((𝜑𝑏𝑣) ↔ (𝜑𝑏𝑎)))
1512, 14opelopab2 4271 . . . . . . . . . 10 ((𝑏 ∈ 2o𝑎 ∈ 2o) → (⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ↔ (𝜑𝑏𝑎)))
1615ancoms 268 . . . . . . . . 9 ((𝑎 ∈ 2o𝑏 ∈ 2o) → (⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ↔ (𝜑𝑏𝑎)))
17 necom 2431 . . . . . . . . . 10 (𝑏𝑎𝑎𝑏)
1817anbi2i 457 . . . . . . . . 9 ((𝜑𝑏𝑎) ↔ (𝜑𝑎𝑏))
1916, 18bitrdi 196 . . . . . . . 8 ((𝑎 ∈ 2o𝑏 ∈ 2o) → (⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ↔ (𝜑𝑎𝑏)))
2010, 19bitrid 192 . . . . . . 7 ((𝑎 ∈ 2o𝑏 ∈ 2o) → (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎 ↔ (𝜑𝑎𝑏)))
219, 20bitr4d 191 . . . . . 6 ((𝑎 ∈ 2o𝑏 ∈ 2o) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎))
2221biimpd 144 . . . . 5 ((𝑎 ∈ 2o𝑏 ∈ 2o) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎))
2322rgen2 2563 . . . 4 𝑎 ∈ 2o𝑏 ∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎)
2423a1i 9 . . 3 (¬ ¬ 𝜑 → ∀𝑎 ∈ 2o𝑏 ∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎))
25 neirr 2356 . . . . . 6 ¬ 𝑎𝑎
2625intnan 929 . . . . 5 ¬ (𝜑𝑎𝑎)
27 df-br 4005 . . . . . 6 (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎 ↔ ⟨𝑎, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))})
28 neeq2 2361 . . . . . . . . 9 (𝑣 = 𝑎 → (𝑎𝑣𝑎𝑎))
2928anbi2d 464 . . . . . . . 8 (𝑣 = 𝑎 → ((𝜑𝑎𝑣) ↔ (𝜑𝑎𝑎)))
305, 29opelopab2 4271 . . . . . . 7 ((𝑎 ∈ 2o𝑎 ∈ 2o) → (⟨𝑎, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ↔ (𝜑𝑎𝑎)))
3130anidms 397 . . . . . 6 (𝑎 ∈ 2o → (⟨𝑎, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ↔ (𝜑𝑎𝑎)))
3227, 31bitrid 192 . . . . 5 (𝑎 ∈ 2o → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎 ↔ (𝜑𝑎𝑎)))
3326, 32mtbiri 675 . . . 4 (𝑎 ∈ 2o → ¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎)
3433rgen 2530 . . 3 𝑎 ∈ 2o ¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎
3524, 34jctil 312 . 2 (¬ ¬ 𝜑 → (∀𝑎 ∈ 2o ¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎 ∧ ∀𝑎 ∈ 2o𝑏 ∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎)))
3693adant3 1017 . . . . . 6 ((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏 ↔ (𝜑𝑎𝑏)))
37 simpr 110 . . . . . . . . . . . 12 ((((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) ∧ 𝑎 = 𝑐) → 𝑎 = 𝑐)
38 simplrr 536 . . . . . . . . . . . 12 ((((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) ∧ 𝑎 = 𝑐) → 𝑎𝑏)
3937, 38eqnetrrd 2373 . . . . . . . . . . 11 ((((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) ∧ 𝑎 = 𝑐) → 𝑐𝑏)
4039necomd 2433 . . . . . . . . . 10 ((((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) ∧ 𝑎 = 𝑐) → 𝑏𝑐)
4140olcd 734 . . . . . . . . 9 ((((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) ∧ 𝑎 = 𝑐) → (𝑎𝑐𝑏𝑐))
42 simpr 110 . . . . . . . . . . 11 ((((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) ∧ ¬ 𝑎 = 𝑐) → ¬ 𝑎 = 𝑐)
4342neqned 2354 . . . . . . . . . 10 ((((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) ∧ ¬ 𝑎 = 𝑐) → 𝑎𝑐)
4443orcd 733 . . . . . . . . 9 ((((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) ∧ ¬ 𝑎 = 𝑐) → (𝑎𝑐𝑏𝑐))
45 simpl1 1000 . . . . . . . . . . . 12 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → 𝑎 ∈ 2o)
46 2onn 6522 . . . . . . . . . . . 12 2o ∈ ω
47 elnn 4606 . . . . . . . . . . . 12 ((𝑎 ∈ 2o ∧ 2o ∈ ω) → 𝑎 ∈ ω)
4845, 46, 47sylancl 413 . . . . . . . . . . 11 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → 𝑎 ∈ ω)
49 simpl3 1002 . . . . . . . . . . . 12 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → 𝑐 ∈ 2o)
50 elnn 4606 . . . . . . . . . . . 12 ((𝑐 ∈ 2o ∧ 2o ∈ ω) → 𝑐 ∈ ω)
5149, 46, 50sylancl 413 . . . . . . . . . . 11 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → 𝑐 ∈ ω)
52 nndceq 6500 . . . . . . . . . . 11 ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) → DECID 𝑎 = 𝑐)
5348, 51, 52syl2anc 411 . . . . . . . . . 10 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → DECID 𝑎 = 𝑐)
54 exmiddc 836 . . . . . . . . . 10 (DECID 𝑎 = 𝑐 → (𝑎 = 𝑐 ∨ ¬ 𝑎 = 𝑐))
5553, 54syl 14 . . . . . . . . 9 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → (𝑎 = 𝑐 ∨ ¬ 𝑎 = 𝑐))
5641, 44, 55mpjaodan 798 . . . . . . . 8 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → (𝑎𝑐𝑏𝑐))
57 df-br 4005 . . . . . . . . . . . 12 (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐 ↔ ⟨𝑎, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))})
58 neeq2 2361 . . . . . . . . . . . . . . 15 (𝑣 = 𝑐 → (𝑎𝑣𝑎𝑐))
5958anbi2d 464 . . . . . . . . . . . . . 14 (𝑣 = 𝑐 → ((𝜑𝑎𝑣) ↔ (𝜑𝑎𝑐)))
605, 59opelopab2 4271 . . . . . . . . . . . . 13 ((𝑎 ∈ 2o𝑐 ∈ 2o) → (⟨𝑎, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ↔ (𝜑𝑎𝑐)))
61603adant2 1016 . . . . . . . . . . . 12 ((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) → (⟨𝑎, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ↔ (𝜑𝑎𝑐)))
6257, 61bitrid 192 . . . . . . . . . . 11 ((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐 ↔ (𝜑𝑎𝑐)))
6362adantr 276 . . . . . . . . . 10 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐 ↔ (𝜑𝑎𝑐)))
64 ibar 301 . . . . . . . . . . . 12 (𝜑 → (𝑎𝑐 ↔ (𝜑𝑎𝑐)))
6564adantr 276 . . . . . . . . . . 11 ((𝜑𝑎𝑏) → (𝑎𝑐 ↔ (𝜑𝑎𝑐)))
6665adantl 277 . . . . . . . . . 10 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → (𝑎𝑐 ↔ (𝜑𝑎𝑐)))
6763, 66bitr4d 191 . . . . . . . . 9 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐𝑎𝑐))
68 df-br 4005 . . . . . . . . . . . 12 (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐 ↔ ⟨𝑏, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))})
69 neeq2 2361 . . . . . . . . . . . . . . 15 (𝑣 = 𝑐 → (𝑏𝑣𝑏𝑐))
7069anbi2d 464 . . . . . . . . . . . . . 14 (𝑣 = 𝑐 → ((𝜑𝑏𝑣) ↔ (𝜑𝑏𝑐)))
7112, 70opelopab2 4271 . . . . . . . . . . . . 13 ((𝑏 ∈ 2o𝑐 ∈ 2o) → (⟨𝑏, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ↔ (𝜑𝑏𝑐)))
72713adant1 1015 . . . . . . . . . . . 12 ((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) → (⟨𝑏, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ↔ (𝜑𝑏𝑐)))
7368, 72bitrid 192 . . . . . . . . . . 11 ((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) → (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐 ↔ (𝜑𝑏𝑐)))
7473adantr 276 . . . . . . . . . 10 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐 ↔ (𝜑𝑏𝑐)))
75 ibar 301 . . . . . . . . . . . 12 (𝜑 → (𝑏𝑐 ↔ (𝜑𝑏𝑐)))
7675adantr 276 . . . . . . . . . . 11 ((𝜑𝑎𝑏) → (𝑏𝑐 ↔ (𝜑𝑏𝑐)))
7776adantl 277 . . . . . . . . . 10 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → (𝑏𝑐 ↔ (𝜑𝑏𝑐)))
7874, 77bitr4d 191 . . . . . . . . 9 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐𝑏𝑐))
7967, 78orbi12d 793 . . . . . . . 8 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → ((𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐) ↔ (𝑎𝑐𝑏𝑐)))
8056, 79mpbird 167 . . . . . . 7 (((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) ∧ (𝜑𝑎𝑏)) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐))
8180ex 115 . . . . . 6 ((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) → ((𝜑𝑎𝑏) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐)))
8236, 81sylbid 150 . . . . 5 ((𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐)))
8382adantl 277 . . . 4 ((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o)) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐)))
8483ralrimivvva 2560 . . 3 (¬ ¬ 𝜑 → ∀𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐)))
859notbid 667 . . . . . 6 ((𝑎 ∈ 2o𝑏 ∈ 2o) → (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏 ↔ ¬ (𝜑𝑎𝑏)))
8685adantl 277 . . . . 5 ((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) → (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏 ↔ ¬ (𝜑𝑎𝑏)))
87 simpll 527 . . . . . . . 8 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → ¬ ¬ 𝜑)
88 simpr 110 . . . . . . . . . 10 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → ¬ (𝜑𝑎𝑏))
89 ancom 266 . . . . . . . . . 10 ((𝜑𝑎𝑏) ↔ (𝑎𝑏𝜑))
9088, 89sylnib 676 . . . . . . . . 9 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → ¬ (𝑎𝑏𝜑))
91 imnan 690 . . . . . . . . 9 ((𝑎𝑏 → ¬ 𝜑) ↔ ¬ (𝑎𝑏𝜑))
9290, 91sylibr 134 . . . . . . . 8 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → (𝑎𝑏 → ¬ 𝜑))
9387, 92mtod 663 . . . . . . 7 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → ¬ 𝑎𝑏)
94 simplrl 535 . . . . . . . . . 10 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → 𝑎 ∈ 2o)
9594, 46, 47sylancl 413 . . . . . . . . 9 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → 𝑎 ∈ ω)
96 simplrr 536 . . . . . . . . . 10 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → 𝑏 ∈ 2o)
97 elnn 4606 . . . . . . . . . 10 ((𝑏 ∈ 2o ∧ 2o ∈ ω) → 𝑏 ∈ ω)
9896, 46, 97sylancl 413 . . . . . . . . 9 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → 𝑏 ∈ ω)
99 nndceq 6500 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → DECID 𝑎 = 𝑏)
10095, 98, 99syl2anc 411 . . . . . . . 8 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → DECID 𝑎 = 𝑏)
101 nnedc 2352 . . . . . . . 8 (DECID 𝑎 = 𝑏 → (¬ 𝑎𝑏𝑎 = 𝑏))
102100, 101syl 14 . . . . . . 7 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → (¬ 𝑎𝑏𝑎 = 𝑏))
10393, 102mpbid 147 . . . . . 6 (((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) ∧ ¬ (𝜑𝑎𝑏)) → 𝑎 = 𝑏)
104103ex 115 . . . . 5 ((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) → (¬ (𝜑𝑎𝑏) → 𝑎 = 𝑏))
10586, 104sylbid 150 . . . 4 ((¬ ¬ 𝜑 ∧ (𝑎 ∈ 2o𝑏 ∈ 2o)) → (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏𝑎 = 𝑏))
106105ralrimivva 2559 . . 3 (¬ ¬ 𝜑 → ∀𝑎 ∈ 2o𝑏 ∈ 2o𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏𝑎 = 𝑏))
10784, 106jca 306 . 2 (¬ ¬ 𝜑 → (∀𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐)) ∧ ∀𝑎 ∈ 2o𝑏 ∈ 2o𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏𝑎 = 𝑏)))
108 dftap2 7250 . 2 ({⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} TAp 2o ↔ ({⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} ⊆ (2o × 2o) ∧ (∀𝑎 ∈ 2o ¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎 ∧ ∀𝑎 ∈ 2o𝑏 ∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑎)) ∧ (∀𝑎 ∈ 2o𝑏 ∈ 2o𝑐 ∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑐)) ∧ ∀𝑎 ∈ 2o𝑏 ∈ 2o𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))}𝑏𝑎 = 𝑏))))
1092, 35, 107, 108syl3anbrc 1181 1 (¬ ¬ 𝜑 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} TAp 2o)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834  w3a 978  wcel 2148  wne 2347  wral 2455  wss 3130  cop 3596   class class class wbr 4004  {copab 4064  ωcom 4590   × cxp 4625  2oc2o 6411   TAp wtap 7248
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 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  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-v 2740  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-br 4005  df-opab 4066  df-tr 4103  df-iord 4367  df-on 4369  df-suc 4372  df-iom 4591  df-xp 4633  df-1o 6417  df-2o 6418  df-pap 7247  df-tap 7249
This theorem is referenced by:  2omotaplemst  7257
  Copyright terms: Public domain W3C validator