Step | Hyp | Ref
| Expression |
1 | | ssn0 4365 |
. . . . . . . . 9
⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅) |
2 | | xpnz 6116 |
. . . . . . . . . . 11
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅) |
3 | 2 | biimpri 227 |
. . . . . . . . . 10
⊢ ((𝐴 × 𝐵) ≠ ∅ → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅)) |
4 | 3 | simprd 497 |
. . . . . . . . 9
⊢ ((𝐴 × 𝐵) ≠ ∅ → 𝐵 ≠ ∅) |
5 | 1, 4 | syl 17 |
. . . . . . . 8
⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → 𝐵 ≠ ∅) |
6 | | dmxp 5889 |
. . . . . . . . . 10
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
7 | | dmss 5863 |
. . . . . . . . . . 11
⊢ (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵)) |
8 | | sseq2 3975 |
. . . . . . . . . . 11
⊢ (dom
(𝐴 × 𝐵) = 𝐴 → (dom 𝑠 ⊆ dom (𝐴 × 𝐵) ↔ dom 𝑠 ⊆ 𝐴)) |
9 | 7, 8 | imbitrid 243 |
. . . . . . . . . 10
⊢ (dom
(𝐴 × 𝐵) = 𝐴 → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ 𝐴)) |
10 | 6, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝐵 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ 𝐴)) |
11 | 10 | impcom 409 |
. . . . . . . 8
⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝐵 ≠ ∅) → dom 𝑠 ⊆ 𝐴) |
12 | 5, 11 | syldan 592 |
. . . . . . 7
⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ⊆ 𝐴) |
13 | | relxp 5656 |
. . . . . . . . . . 11
⊢ Rel
(𝐴 × 𝐵) |
14 | | relss 5742 |
. . . . . . . . . . 11
⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠)) |
15 | 13, 14 | mpi 20 |
. . . . . . . . . 10
⊢ (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠) |
16 | | reldm0 5888 |
. . . . . . . . . 10
⊢ (Rel
𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅)) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 = ∅ ↔ dom 𝑠 = ∅)) |
18 | 17 | necon3bid 2989 |
. . . . . . . 8
⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅)) |
19 | 18 | biimpa 478 |
. . . . . . 7
⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ≠ ∅) |
20 | 12, 19 | jca 513 |
. . . . . 6
⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅)) |
21 | | df-fr 5593 |
. . . . . . 7
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑣((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎)) |
22 | | vex 3452 |
. . . . . . . . 9
⊢ 𝑠 ∈ V |
23 | 22 | dmex 7853 |
. . . . . . . 8
⊢ dom 𝑠 ∈ V |
24 | | sseq1 3974 |
. . . . . . . . . 10
⊢ (𝑣 = dom 𝑠 → (𝑣 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴)) |
25 | | neeq1 3007 |
. . . . . . . . . 10
⊢ (𝑣 = dom 𝑠 → (𝑣 ≠ ∅ ↔ dom 𝑠 ≠ ∅)) |
26 | 24, 25 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑣 = dom 𝑠 → ((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) ↔ (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅))) |
27 | | raleq 3312 |
. . . . . . . . . 10
⊢ (𝑣 = dom 𝑠 → (∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎 ↔ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)) |
28 | 27 | rexeqbi1dv 3311 |
. . . . . . . . 9
⊢ (𝑣 = dom 𝑠 → (∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)) |
29 | 26, 28 | imbi12d 345 |
. . . . . . . 8
⊢ (𝑣 = dom 𝑠 → (((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎) ↔ ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))) |
30 | 23, 29 | spcv 3567 |
. . . . . . 7
⊢
(∀𝑣((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)) |
31 | 21, 30 | sylbi 216 |
. . . . . 6
⊢ (𝑅 Fr 𝐴 → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)) |
32 | 20, 31 | syl5 34 |
. . . . 5
⊢ (𝑅 Fr 𝐴 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)) |
33 | 32 | adantr 482 |
. . . 4
⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)) |
34 | | imassrn 6029 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 “ {𝑎}) ⊆ ran 𝑠 |
35 | | xpeq0 6117 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅)) |
36 | 35 | biimpri 227 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅) |
37 | 36 | orcs 874 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = ∅ → (𝐴 × 𝐵) = ∅) |
38 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) ↔ 𝑠 ⊆ ∅)) |
39 | | ss0 4363 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ⊆ ∅ → 𝑠 = ∅) |
40 | 38, 39 | syl6bi 253 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅)) |
41 | 37, 40 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅)) |
42 | | rneq 5896 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = ∅ → ran 𝑠 = ran ∅) |
43 | | rn0 5886 |
. . . . . . . . . . . . . . . . . . 19
⊢ ran
∅ = ∅ |
44 | | 0ss 4361 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∅
⊆ 𝐵 |
45 | 43, 44 | eqsstri 3983 |
. . . . . . . . . . . . . . . . . 18
⊢ ran
∅ ⊆ 𝐵 |
46 | 42, 45 | eqsstrdi 4003 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = ∅ → ran 𝑠 ⊆ 𝐵) |
47 | 41, 46 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵)) |
48 | | rnxp 6127 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) |
49 | | rnss 5899 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵)) |
50 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
(𝐴 × 𝐵) = 𝐵 → (ran 𝑠 ⊆ ran (𝐴 × 𝐵) ↔ ran 𝑠 ⊆ 𝐵)) |
51 | 49, 50 | imbitrid 243 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(𝐴 × 𝐵) = 𝐵 → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵)) |
52 | 48, 51 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵)) |
53 | 47, 52 | pm2.61ine 3029 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵) |
54 | 34, 53 | sstrid 3960 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 “ {𝑎}) ⊆ 𝐵) |
55 | | vex 3452 |
. . . . . . . . . . . . . . . 16
⊢ 𝑎 ∈ V |
56 | 55 | eldm 5861 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ dom 𝑠 ↔ ∃𝑏 𝑎𝑠𝑏) |
57 | | vex 3452 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑏 ∈ V |
58 | 55, 57 | elimasn 6046 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠) |
59 | | df-br 5111 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎𝑠𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠) |
60 | 58, 59 | bitr4i 278 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ (𝑠 “ {𝑎}) ↔ 𝑎𝑠𝑏) |
61 | | ne0i 4299 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ (𝑠 “ {𝑎}) → (𝑠 “ {𝑎}) ≠ ∅) |
62 | 60, 61 | sylbir 234 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅) |
63 | 62 | exlimiv 1934 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑏 𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅) |
64 | 56, 63 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ dom 𝑠 → (𝑠 “ {𝑎}) ≠ ∅) |
65 | | df-fr 5593 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 Fr 𝐵 ↔ ∀𝑣((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏)) |
66 | 22 | imaex 7858 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 “ {𝑎}) ∈ V |
67 | | sseq1 3974 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ⊆ 𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵)) |
68 | | neeq1 3007 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅)) |
69 | 67, 68 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝑠 “ {𝑎}) → ((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅))) |
70 | | raleq 3312 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝑠 “ {𝑎}) → (∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)) |
71 | 70 | rexeqbi1dv 3311 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝑠 “ {𝑎}) → (∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏 ↔ ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)) |
72 | 69, 71 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = (𝑠 “ {𝑎}) → (((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))) |
73 | 66, 72 | spcv 3567 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)) |
74 | 65, 73 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢ (𝑆 Fr 𝐵 → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)) |
75 | 54, 64, 74 | syl2ani 608 |
. . . . . . . . . . . . 13
⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)) |
76 | | 1stdm 7977 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Rel
𝑠 ∧ 𝑤 ∈ 𝑠) → (1st ‘𝑤) ∈ dom 𝑠) |
77 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 = (1st ‘𝑤) → (𝑐𝑅𝑎 ↔ (1st ‘𝑤)𝑅𝑎)) |
78 | 77 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 = (1st ‘𝑤) → (¬ 𝑐𝑅𝑎 ↔ ¬ (1st ‘𝑤)𝑅𝑎)) |
79 | 78 | rspccv 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑐 ∈
dom 𝑠 ¬ 𝑐𝑅𝑎 → ((1st ‘𝑤) ∈ dom 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎)) |
80 | 76, 79 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑐 ∈
dom 𝑠 ¬ 𝑐𝑅𝑎 → ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → ¬ (1st ‘𝑤)𝑅𝑎)) |
81 | 80 | expd 417 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑐 ∈
dom 𝑠 ¬ 𝑐𝑅𝑎 → (Rel 𝑠 → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎))) |
82 | 81 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Rel
𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎)) |
83 | 82 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((Rel
𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎)) |
84 | | elrel 5759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Rel
𝑠 ∧ 𝑤 ∈ 𝑠) → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩) |
85 | 84 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (Rel
𝑠 → (𝑤 ∈ 𝑠 → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩)) |
86 | 85 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Rel
𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩)) |
87 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 𝑢 ∈ V |
88 | 55, 87 | elimasn 6046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑢 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠) |
89 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑑 = 𝑢 → (𝑑𝑆𝑏 ↔ 𝑢𝑆𝑏)) |
90 | 89 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑑 = 𝑢 → (¬ 𝑑𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏)) |
91 | 90 | rspccv 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∀𝑑 ∈
(𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (𝑢 ∈ (𝑠 “ {𝑎}) → ¬ 𝑢𝑆𝑏)) |
92 | 88, 91 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∀𝑑 ∈
(𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)) |
93 | 92 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((Rel
𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)) |
94 | | opeq1 4835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 = 𝑎 → ⟨𝑡, 𝑢⟩ = ⟨𝑎, 𝑢⟩) |
95 | 94 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 = 𝑎 → (⟨𝑡, 𝑢⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠)) |
96 | 95 | imbi1d 342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑡 = 𝑎 → ((⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏) ↔ (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))) |
97 | 93, 96 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 𝑎 → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))) |
98 | 97 | com3l 89 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Rel
𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏))) |
99 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (𝑤 ∈ 𝑠 ↔ ⟨𝑡, 𝑢⟩ ∈ 𝑠)) |
100 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 𝑡 ∈ V |
101 | 100, 87 | op1std 7936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (1st ‘𝑤) = 𝑡) |
102 | 101 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((1st ‘𝑤) = 𝑎 ↔ 𝑡 = 𝑎)) |
103 | 100, 87 | op2ndd 7937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (2nd ‘𝑤) = 𝑢) |
104 | 103 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((2nd ‘𝑤)𝑆𝑏 ↔ 𝑢𝑆𝑏)) |
105 | 104 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (¬ (2nd
‘𝑤)𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏)) |
106 | 102, 105 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏) ↔ (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏))) |
107 | 99, 106 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) ↔ (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))) |
108 | 98, 107 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))) |
109 | 108 | exlimivv 1936 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))) |
110 | 109 | com3l 89 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Rel
𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → (∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))) |
111 | 86, 110 | mpdd 43 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Rel
𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))) |
112 | 111 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((Rel
𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))) |
113 | 83, 112 | jcad 514 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Rel
𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))) |
114 | 113 | ralrimiv 3143 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Rel
𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))) |
115 | 114 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Rel
𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))) |
116 | 15, 115 | sylan 581 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))) |
117 | | olc 867 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
(1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) → (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))) |
118 | 117 | ralimi 3087 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑤 ∈
𝑠 (¬ (1st
‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) → ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))) |
119 | 116, 118 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))) |
120 | | ianor 981 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))) |
121 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑤 ∈ V |
122 | | opex 5426 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
⟨𝑎, 𝑏⟩ ∈ V |
123 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑤 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 𝑤 ∈ (𝐴 × 𝐵))) |
124 | 123 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)))) |
125 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑤 → (1st ‘𝑥) = (1st ‘𝑤)) |
126 | 125 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑤 → ((1st ‘𝑥)𝑅(1st ‘𝑦) ↔ (1st ‘𝑤)𝑅(1st ‘𝑦))) |
127 | 125 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑤 → ((1st ‘𝑥) = (1st ‘𝑦) ↔ (1st
‘𝑤) = (1st
‘𝑦))) |
128 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑤 → (2nd ‘𝑥) = (2nd ‘𝑤)) |
129 | 128 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑤 → ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ↔ (2nd ‘𝑤)𝑆(2nd ‘𝑦))) |
130 | 127, 129 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑤 → (((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥)𝑆(2nd ‘𝑦)) ↔ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd
‘𝑤)𝑆(2nd ‘𝑦)))) |
131 | 126, 130 | orbi12d 918 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥)𝑆(2nd ‘𝑦))) ↔ ((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd
‘𝑤)𝑆(2nd ‘𝑦))))) |
132 | 124, 131 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥)𝑆(2nd ‘𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd
‘𝑤)𝑆(2nd ‘𝑦)))))) |
133 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵))) |
134 | 133 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))) |
135 | 55, 57 | op1std 7936 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (1st ‘𝑦) = 𝑎) |
136 | 135 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st ‘𝑤)𝑅(1st ‘𝑦) ↔ (1st ‘𝑤)𝑅𝑎)) |
137 | 135 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st ‘𝑤) = (1st ‘𝑦) ↔ (1st
‘𝑤) = 𝑎)) |
138 | 55, 57 | op2ndd 7937 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd ‘𝑦) = 𝑏) |
139 | 138 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd ‘𝑤)𝑆(2nd ‘𝑦) ↔ (2nd ‘𝑤)𝑆𝑏)) |
140 | 137, 139 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd
‘𝑤)𝑆(2nd ‘𝑦)) ↔ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) |
141 | 136, 140 | orbi12d 918 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd
‘𝑤)𝑆(2nd ‘𝑦))) ↔ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))) |
142 | 134, 141 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd
‘𝑤)𝑆(2nd ‘𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))) |
143 | | frxp.1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥)𝑆(2nd ‘𝑦))))} |
144 | 121, 122,
132, 142, 143 | brab 5505 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))) |
145 | 120, 144 | xchnxbir 333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑤𝑇⟨𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))) |
146 | | ioran 983 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) |
147 | | ianor 981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
((1st ‘𝑤)
= 𝑎 ∧ (2nd
‘𝑤)𝑆𝑏) ↔ (¬ (1st ‘𝑤) = 𝑎 ∨ ¬ (2nd ‘𝑤)𝑆𝑏)) |
148 | | pm4.62 855 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏) ↔ (¬ (1st ‘𝑤) = 𝑎 ∨ ¬ (2nd ‘𝑤)𝑆𝑏)) |
149 | 147, 148 | bitr4i 278 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
((1st ‘𝑤)
= 𝑎 ∧ (2nd
‘𝑤)𝑆𝑏) ↔ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) |
150 | 149 | anbi2i 624 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((¬
(1st ‘𝑤)𝑅𝑎 ∧ ¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))) |
151 | 146, 150 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))) |
152 | 151 | orbi2i 912 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
(𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))) |
153 | 145, 152 | bitri 275 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑤𝑇⟨𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))) |
154 | 153 | ralbii 3097 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑤 ∈
𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))) |
155 | 119, 154 | syl6ibr 252 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) |
156 | 155 | reximdv 3168 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) |
157 | 156 | ex 414 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))) |
158 | 157 | com23 86 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))) |
159 | 158 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))) |
160 | 75, 159 | sylcom 30 |
. . . . . . . . . . . 12
⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))) |
161 | 160 | impl 457 |
. . . . . . . . . . 11
⊢ (((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵)) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) |
162 | 161 | expimpd 455 |
. . . . . . . . . 10
⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵)) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) |
163 | 162 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) |
164 | | resss 5967 |
. . . . . . . . . 10
⊢ (𝑠 ↾ {𝑎}) ⊆ 𝑠 |
165 | | df-rex 3075 |
. . . . . . . . . . . . 13
⊢
(∃𝑏 ∈
(𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) |
166 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ |
167 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩)) |
168 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑤𝑇𝑧 ↔ 𝑤𝑇⟨𝑎, 𝑏⟩)) |
169 | 168 | notbid 318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (¬ 𝑤𝑇𝑧 ↔ ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) |
170 | 169 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) |
171 | 170 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))) |
172 | 167, 171 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) ↔ (⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))) |
173 | 122, 172 | spcev 3568 |
. . . . . . . . . . . . . . . 16
⊢
((⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
174 | 166, 173 | mpan 689 |
. . . . . . . . . . . . . . 15
⊢
((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
175 | 58, 174 | sylanb 582 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
176 | 175 | eximi 1838 |
. . . . . . . . . . . . 13
⊢
(∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
177 | 165, 176 | sylbi 216 |
. . . . . . . . . . . 12
⊢
(∃𝑏 ∈
(𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
178 | | excom 2163 |
. . . . . . . . . . . 12
⊢
(∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
179 | 177, 178 | sylib 217 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
(𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
180 | | df-rex 3075 |
. . . . . . . . . . . 12
⊢
(∃𝑧 ∈
(𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) |
181 | 55 | elsnres 5982 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝑠 ↾ {𝑎}) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠)) |
182 | 181 | anbi1i 625 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) |
183 | | 19.41v 1954 |
. . . . . . . . . . . . . 14
⊢
(∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) |
184 | | anass 470 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
185 | 184 | exbii 1851 |
. . . . . . . . . . . . . 14
⊢
(∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
186 | 182, 183,
185 | 3bitr2i 299 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
187 | 186 | exbii 1851 |
. . . . . . . . . . . 12
⊢
(∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
188 | 180, 187 | bitri 275 |
. . . . . . . . . . 11
⊢
(∃𝑧 ∈
(𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
189 | 179, 188 | sylibr 233 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
(𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) |
190 | | ssrexv 4016 |
. . . . . . . . . 10
⊢ ((𝑠 ↾ {𝑎}) ⊆ 𝑠 → (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) |
191 | 164, 189,
190 | mpsyl 68 |
. . . . . . . . 9
⊢
(∃𝑏 ∈
(𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) |
192 | 163, 191 | syl6 35 |
. . . . . . . 8
⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) |
193 | 192 | expd 417 |
. . . . . . 7
⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝑎 ∈ dom 𝑠 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
194 | 193 | rexlimdv 3151 |
. . . . . 6
⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) |
195 | 194 | 3expib 1123 |
. . . . 5
⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
196 | 195 | adantl 483 |
. . . 4
⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))) |
197 | 33, 196 | mpdd 43 |
. . 3
⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) |
198 | 197 | alrimiv 1931 |
. 2
⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) |
199 | | df-fr 5593 |
. 2
⊢ (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) |
200 | 198, 199 | sylibr 233 |
1
⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵)) |