Step | Hyp | Ref
| Expression |
1 | | dmss 5745 |
. . . . . . . . . 10
⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶)) |
2 | 1 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶)) |
3 | | dmxpss 6003 |
. . . . . . . . 9
⊢ dom
((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵) |
4 | 2, 3 | sstrdi 3889 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ (𝐴 × 𝐵)) |
5 | | dmss 5745 |
. . . . . . . 8
⊢ (dom
𝑠 ⊆ (𝐴 × 𝐵) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵)) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵)) |
7 | | dmxpss 6003 |
. . . . . . 7
⊢ dom
(𝐴 × 𝐵) ⊆ 𝐴 |
8 | 6, 7 | sstrdi 3889 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ 𝐴) |
9 | | simprr 773 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑠 ≠ ∅) |
10 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) |
11 | | relxp 5543 |
. . . . . . . . . . 11
⊢ Rel
((𝐴 × 𝐵) × 𝐶) |
12 | | relss 5627 |
. . . . . . . . . . 11
⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → (Rel ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠)) |
13 | 10, 11, 12 | mpisyl 21 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → Rel 𝑠) |
14 | | reldm0 5771 |
. . . . . . . . . 10
⊢ (Rel
𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅)) |
16 | 15 | necon3bid 2978 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅)) |
17 | 9, 16 | mpbid 235 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ≠ ∅) |
18 | | relxp 5543 |
. . . . . . . . . 10
⊢ Rel
(𝐴 × 𝐵) |
19 | | relss 5627 |
. . . . . . . . . 10
⊢ (dom
𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel dom 𝑠)) |
20 | 4, 18, 19 | mpisyl 21 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → Rel dom 𝑠) |
21 | | reldm0 5771 |
. . . . . . . . 9
⊢ (Rel dom
𝑠 → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅)) |
22 | 20, 21 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅)) |
23 | 22 | necon3bid 2978 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 ≠ ∅ ↔ dom dom
𝑠 ≠
∅)) |
24 | 17, 23 | mpbid 235 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ≠ ∅) |
25 | | frxp3.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 Fr 𝐴) |
26 | | df-fr 5483 |
. . . . . . . . 9
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑔((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎)) |
27 | 25, 26 | sylib 221 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑔((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎)) |
28 | 27 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∀𝑔((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎)) |
29 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑠 ∈ V |
30 | 29 | dmex 7642 |
. . . . . . . . 9
⊢ dom 𝑠 ∈ V |
31 | 30 | dmex 7642 |
. . . . . . . 8
⊢ dom dom
𝑠 ∈ V |
32 | | sseq1 3902 |
. . . . . . . . . 10
⊢ (𝑔 = dom dom 𝑠 → (𝑔 ⊆ 𝐴 ↔ dom dom 𝑠 ⊆ 𝐴)) |
33 | | neeq1 2996 |
. . . . . . . . . 10
⊢ (𝑔 = dom dom 𝑠 → (𝑔 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅)) |
34 | 32, 33 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑔 = dom dom 𝑠 → ((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) ↔ (dom dom 𝑠 ⊆ 𝐴 ∧ dom dom 𝑠 ≠ ∅))) |
35 | | raleq 3310 |
. . . . . . . . . 10
⊢ (𝑔 = dom dom 𝑠 → (∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎 ↔ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) |
36 | 35 | rexeqbi1dv 3309 |
. . . . . . . . 9
⊢ (𝑔 = dom dom 𝑠 → (∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎 ↔ ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) |
37 | 34, 36 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑔 = dom dom 𝑠 → (((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎) ↔ ((dom dom 𝑠 ⊆ 𝐴 ∧ dom dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎))) |
38 | 31, 37 | spcv 3509 |
. . . . . . 7
⊢
(∀𝑔((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎) → ((dom dom 𝑠 ⊆ 𝐴 ∧ dom dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) |
39 | 28, 38 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ((dom dom 𝑠 ⊆ 𝐴 ∧ dom dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) |
40 | 8, 24, 39 | mp2and 699 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎) |
41 | | imassrn 5914 |
. . . . . . . 8
⊢ (dom
𝑠 “ {𝑎}) ⊆ ran dom 𝑠 |
42 | | rnss 5782 |
. . . . . . . . . . 11
⊢ (dom
𝑠 ⊆ (𝐴 × 𝐵) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵)) |
43 | 4, 42 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵)) |
44 | | rnxpss 6004 |
. . . . . . . . . 10
⊢ ran
(𝐴 × 𝐵) ⊆ 𝐵 |
45 | 43, 44 | sstrdi 3889 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ 𝐵) |
46 | 45 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ran dom 𝑠 ⊆ 𝐵) |
47 | 41, 46 | sstrid 3888 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ⊆ 𝐵) |
48 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑎 ∈ dom dom 𝑠) |
49 | | imadisj 5922 |
. . . . . . . . . 10
⊢ ((dom
𝑠 “ {𝑎}) = ∅ ↔ (dom dom
𝑠 ∩ {𝑎}) = ∅) |
50 | | disjsn 4602 |
. . . . . . . . . 10
⊢ ((dom dom
𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠) |
51 | 49, 50 | bitri 278 |
. . . . . . . . 9
⊢ ((dom
𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠) |
52 | 51 | necon2abii 2984 |
. . . . . . . 8
⊢ (𝑎 ∈ dom dom 𝑠 ↔ (dom 𝑠 “ {𝑎}) ≠ ∅) |
53 | 48, 52 | sylib 221 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ≠ ∅) |
54 | | frxp3.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 Fr 𝐵) |
55 | | df-fr 5483 |
. . . . . . . . . 10
⊢ (𝑆 Fr 𝐵 ↔ ∀𝑔((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏)) |
56 | 54, 55 | sylib 221 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑔((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏)) |
57 | 30 | imaex 7647 |
. . . . . . . . . 10
⊢ (dom
𝑠 “ {𝑎}) ∈ V |
58 | | sseq1 3902 |
. . . . . . . . . . . 12
⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (𝑔 ⊆ 𝐵 ↔ (dom 𝑠 “ {𝑎}) ⊆ 𝐵)) |
59 | | neeq1 2996 |
. . . . . . . . . . . 12
⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (𝑔 ≠ ∅ ↔ (dom 𝑠 “ {𝑎}) ≠ ∅)) |
60 | 58, 59 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → ((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) ↔ ((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅))) |
61 | | raleq 3310 |
. . . . . . . . . . . 12
⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏 ↔ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) |
62 | 61 | rexeqbi1dv 3309 |
. . . . . . . . . . 11
⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏 ↔ ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) |
63 | 60, 62 | imbi12d 348 |
. . . . . . . . . 10
⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏) ↔ (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))) |
64 | 57, 63 | spcv 3509 |
. . . . . . . . 9
⊢
(∀𝑔((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏) → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) |
65 | 56, 64 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) |
66 | 65 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) |
67 | 47, 53, 66 | mp2and 699 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏) |
68 | | imassrn 5914 |
. . . . . . . . . 10
⊢ (𝑠 “ {〈𝑎, 𝑏〉}) ⊆ ran 𝑠 |
69 | | rnss 5782 |
. . . . . . . . . . . 12
⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶)) |
70 | 69 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶)) |
71 | | rnxpss 6004 |
. . . . . . . . . . 11
⊢ ran
((𝐴 × 𝐵) × 𝐶) ⊆ 𝐶 |
72 | 70, 71 | sstrdi 3889 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ 𝐶) |
73 | 68, 72 | sstrid 3888 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 “ {〈𝑎, 𝑏〉}) ⊆ 𝐶) |
74 | 73 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {〈𝑎, 𝑏〉}) ⊆ 𝐶) |
75 | | simprl 771 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 𝑏 ∈ (dom 𝑠 “ {𝑎})) |
76 | | vex 3402 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
77 | | vex 3402 |
. . . . . . . . . . 11
⊢ 𝑏 ∈ V |
78 | 76, 77 | elimasn 5928 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ↔ 〈𝑎, 𝑏〉 ∈ dom 𝑠) |
79 | 75, 78 | sylib 221 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 〈𝑎, 𝑏〉 ∈ dom 𝑠) |
80 | | imadisj 5922 |
. . . . . . . . . . 11
⊢ ((𝑠 “ {〈𝑎, 𝑏〉}) = ∅ ↔ (dom 𝑠 ∩ {〈𝑎, 𝑏〉}) = ∅) |
81 | | disjsn 4602 |
. . . . . . . . . . 11
⊢ ((dom
𝑠 ∩ {〈𝑎, 𝑏〉}) = ∅ ↔ ¬ 〈𝑎, 𝑏〉 ∈ dom 𝑠) |
82 | 80, 81 | bitri 278 |
. . . . . . . . . 10
⊢ ((𝑠 “ {〈𝑎, 𝑏〉}) = ∅ ↔ ¬ 〈𝑎, 𝑏〉 ∈ dom 𝑠) |
83 | 82 | necon2abii 2984 |
. . . . . . . . 9
⊢
(〈𝑎, 𝑏〉 ∈ dom 𝑠 ↔ (𝑠 “ {〈𝑎, 𝑏〉}) ≠ ∅) |
84 | 79, 83 | sylib 221 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {〈𝑎, 𝑏〉}) ≠ ∅) |
85 | | frxp3.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 Fr 𝐶) |
86 | | df-fr 5483 |
. . . . . . . . . . 11
⊢ (𝑇 Fr 𝐶 ↔ ∀𝑔((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐)) |
87 | 85, 86 | sylib 221 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑔((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐)) |
88 | 29 | imaex 7647 |
. . . . . . . . . . 11
⊢ (𝑠 “ {〈𝑎, 𝑏〉}) ∈ V |
89 | | sseq1 3902 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑠 “ {〈𝑎, 𝑏〉}) → (𝑔 ⊆ 𝐶 ↔ (𝑠 “ {〈𝑎, 𝑏〉}) ⊆ 𝐶)) |
90 | | neeq1 2996 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑠 “ {〈𝑎, 𝑏〉}) → (𝑔 ≠ ∅ ↔ (𝑠 “ {〈𝑎, 𝑏〉}) ≠ ∅)) |
91 | 89, 90 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑠 “ {〈𝑎, 𝑏〉}) → ((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) ↔ ((𝑠 “ {〈𝑎, 𝑏〉}) ⊆ 𝐶 ∧ (𝑠 “ {〈𝑎, 𝑏〉}) ≠ ∅))) |
92 | | raleq 3310 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑠 “ {〈𝑎, 𝑏〉}) → (∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐 ↔ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) |
93 | 92 | rexeqbi1dv 3309 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑠 “ {〈𝑎, 𝑏〉}) → (∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐 ↔ ∃𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉})∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) |
94 | 91, 93 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝑠 “ {〈𝑎, 𝑏〉}) → (((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐) ↔ (((𝑠 “ {〈𝑎, 𝑏〉}) ⊆ 𝐶 ∧ (𝑠 “ {〈𝑎, 𝑏〉}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉})∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐))) |
95 | 88, 94 | spcv 3509 |
. . . . . . . . . 10
⊢
(∀𝑔((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐) → (((𝑠 “ {〈𝑎, 𝑏〉}) ⊆ 𝐶 ∧ (𝑠 “ {〈𝑎, 𝑏〉}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉})∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) |
96 | 87, 95 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑠 “ {〈𝑎, 𝑏〉}) ⊆ 𝐶 ∧ (𝑠 “ {〈𝑎, 𝑏〉}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉})∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) |
97 | 96 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (((𝑠 “ {〈𝑎, 𝑏〉}) ⊆ 𝐶 ∧ (𝑠 “ {〈𝑎, 𝑏〉}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉})∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) |
98 | 74, 84, 97 | mp2and 699 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉})∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐) |
99 | | simprl 771 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → 𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉})) |
100 | | opex 5322 |
. . . . . . . . . 10
⊢
〈𝑎, 𝑏〉 ∈ V |
101 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑐 ∈ V |
102 | 100, 101 | elimasn 5928 |
. . . . . . . . 9
⊢ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ↔ 〈〈𝑎, 𝑏〉, 𝑐〉 ∈ 𝑠) |
103 | 99, 102 | sylib 221 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → 〈〈𝑎, 𝑏〉, 𝑐〉 ∈ 𝑠) |
104 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) |
105 | 104 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) |
106 | | elxpxpss 33258 |
. . . . . . . . . . 11
⊢ ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ 𝑠) → ∃𝑔∃ℎ∃𝑖 𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉) |
107 | 105, 106 | sylan 583 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ∃𝑔∃ℎ∃𝑖 𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉) |
108 | | df-ne 2935 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ≠ 𝑐 ↔ ¬ 𝑖 = 𝑐) |
109 | 108 | con2bii 361 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = 𝑐 ↔ ¬ 𝑖 ≠ 𝑐) |
110 | 109 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = 𝑐 → ¬ 𝑖 ≠ 𝑐) |
111 | 110 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ 𝑖 ≠ 𝑐) |
112 | 111 | intnand 492 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)) |
113 | | breq1 5033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = 𝑖 → (𝑓𝑇𝑐 ↔ 𝑖𝑇𝑐)) |
114 | 113 | notbid 321 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑖 → (¬ 𝑓𝑇𝑐 ↔ ¬ 𝑖𝑇𝑐)) |
115 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) → ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐) |
116 | 115 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐) |
117 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) |
118 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑖 ∈ V |
119 | 100, 118 | elimasn 5928 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ↔ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) |
120 | 117, 119 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 𝑖 ∈ (𝑠 “ {〈𝑎, 𝑏〉})) |
121 | 114, 116,
120 | rspcdva 3528 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ 𝑖𝑇𝑐) |
122 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐) |
123 | 122 | neneqd 2939 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ 𝑖 = 𝑐) |
124 | | ioran 983 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
(𝑖𝑇𝑐 ∨ 𝑖 = 𝑐) ↔ (¬ 𝑖𝑇𝑐 ∧ ¬ 𝑖 = 𝑐)) |
125 | 121, 123,
124 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) |
126 | 125 | intn3an3d 1482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐))) |
127 | 126 | intnanrd 493 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)) |
128 | 112, 127 | pm2.61dane 3021 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)) |
129 | | opeq2 4761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ = 𝑏 → 〈𝑎, ℎ〉 = 〈𝑎, 𝑏〉) |
130 | 129 | opeq1d 4767 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ = 𝑏 → 〈〈𝑎, ℎ〉, 𝑖〉 = 〈〈𝑎, 𝑏〉, 𝑖〉) |
131 | 130 | eleq1d 2817 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = 𝑏 → (〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠 ↔ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠)) |
132 | 131 | anbi2d 632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠))) |
133 | | neeq1 2996 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ = 𝑏 → (ℎ ≠ 𝑏 ↔ 𝑏 ≠ 𝑏)) |
134 | 133 | orbi1d 916 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ = 𝑏 → ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
135 | | neirr 2943 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ¬
𝑏 ≠ 𝑏 |
136 | | orel1 888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝑏 ≠ 𝑏 → ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐)) |
137 | 135, 136 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐) |
138 | | olc 867 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ≠ 𝑐 → (𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) |
139 | 137, 138 | impbii 212 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ 𝑖 ≠ 𝑐) |
140 | 134, 139 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ = 𝑏 → ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ 𝑖 ≠ 𝑐)) |
141 | 140 | anbi2d 632 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = 𝑏 → ((((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))) |
142 | 141 | notbid 321 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = 𝑏 → (¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))) |
143 | 132, 142 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = 𝑏 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)))) |
144 | 128, 143 | mpbiri 261 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
145 | 144 | impcom 411 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ ℎ = 𝑏) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
146 | | breq1 5033 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑒 = ℎ → (𝑒𝑆𝑏 ↔ ℎ𝑆𝑏)) |
147 | 146 | notbid 321 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑒 = ℎ → (¬ 𝑒𝑆𝑏 ↔ ¬ ℎ𝑆𝑏)) |
148 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏) |
149 | 148 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏) |
150 | | opex 5322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
〈𝑎, ℎ〉 ∈ V |
151 | 150, 118 | opeldm 5750 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈〈𝑎,
ℎ〉, 𝑖〉 ∈ 𝑠 → 〈𝑎, ℎ〉 ∈ dom 𝑠) |
152 | 151 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) → 〈𝑎, ℎ〉 ∈ dom 𝑠) |
153 | 152 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → 〈𝑎, ℎ〉 ∈ dom 𝑠) |
154 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ℎ ∈ V |
155 | 76, 154 | elimasn 5928 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ ∈ (dom 𝑠 “ {𝑎}) ↔ 〈𝑎, ℎ〉 ∈ dom 𝑠) |
156 | 153, 155 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ℎ ∈ (dom 𝑠 “ {𝑎})) |
157 | 147, 149,
156 | rspcdva 3528 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ℎ𝑆𝑏) |
158 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ℎ ≠ 𝑏) |
159 | 158 | neneqd 2939 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ℎ = 𝑏) |
160 | | ioran 983 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
(ℎ𝑆𝑏 ∨ ℎ = 𝑏) ↔ (¬ ℎ𝑆𝑏 ∧ ¬ ℎ = 𝑏)) |
161 | 157, 159,
160 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ (ℎ𝑆𝑏 ∨ ℎ = 𝑏)) |
162 | 161 | intn3an2d 1481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐))) |
163 | 162 | intnanrd 493 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
164 | 145, 163 | pm2.61dane 3021 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
165 | | opeq1 4759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔 = 𝑎 → 〈𝑔, ℎ〉 = 〈𝑎, ℎ〉) |
166 | 165 | opeq1d 4767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑎 → 〈〈𝑔, ℎ〉, 𝑖〉 = 〈〈𝑎, ℎ〉, 𝑖〉) |
167 | 166 | eleq1d 2817 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑎 → (〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠 ↔ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠)) |
168 | 167 | anbi2d 632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠))) |
169 | | 3orass 1091 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑔 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
170 | | neeq1 2996 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔 = 𝑎 → (𝑔 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎)) |
171 | 170 | orbi1d 916 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
172 | 169, 171 | syl5bb 286 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
173 | | neirr 2943 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ¬
𝑎 ≠ 𝑎 |
174 | | orel1 888 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑎 ≠ 𝑎 → ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) → (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
175 | 173, 174 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) → (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) |
176 | | olc 867 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
177 | 175, 176 | impbii 212 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) |
178 | 172, 177 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
179 | 178 | anbi2d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑎 → ((((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
180 | 179 | notbid 321 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑎 → (¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
181 | 168, 180 | imbi12d 348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑎 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))) |
182 | 164, 181 | mpbiri 261 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
183 | 182 | impcom 411 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ 𝑔 = 𝑎) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
184 | | breq1 5033 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 = 𝑔 → (𝑑𝑅𝑎 ↔ 𝑔𝑅𝑎)) |
185 | 184 | notbid 321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = 𝑔 → (¬ 𝑑𝑅𝑎 ↔ ¬ 𝑔𝑅𝑎)) |
186 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎) |
187 | 186 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎) |
188 | | opex 5322 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
〈𝑔, ℎ〉 ∈ V |
189 | 188, 118 | opeldm 5750 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈〈𝑔,
ℎ〉, 𝑖〉 ∈ 𝑠 → 〈𝑔, ℎ〉 ∈ dom 𝑠) |
190 | 189 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) → 〈𝑔, ℎ〉 ∈ dom 𝑠) |
191 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑔 ∈ V |
192 | 191, 154 | opeldm 5750 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈𝑔, ℎ〉 ∈ dom 𝑠 → 𝑔 ∈ dom dom 𝑠) |
193 | 190, 192 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) → 𝑔 ∈ dom dom 𝑠) |
194 | 193 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 𝑔 ∈ dom dom 𝑠) |
195 | 185, 187,
194 | rspcdva 3528 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ 𝑔𝑅𝑎) |
196 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 𝑔 ≠ 𝑎) |
197 | 196 | neneqd 2939 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ 𝑔 = 𝑎) |
198 | | ioran 983 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ↔ (¬ 𝑔𝑅𝑎 ∧ ¬ 𝑔 = 𝑎)) |
199 | 195, 197,
198 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ (𝑔𝑅𝑎 ∨ 𝑔 = 𝑎)) |
200 | 199 | intn3an1d 1480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐))) |
201 | 200 | intnanrd 493 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
202 | 183, 201 | pm2.61dane 3021 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
203 | 202 | intn3an3d 1482 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) → ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
204 | | eleq1 2820 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉 → (𝑞 ∈ 𝑠 ↔ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠)) |
205 | 204 | anbi2d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠))) |
206 | | breq1 5033 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉 → (𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ 〈〈𝑔, ℎ〉, 𝑖〉𝑈〈〈𝑎, 𝑏〉, 𝑐〉)) |
207 | | xpord3.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} |
208 | 207 | xpord3lem 33406 |
. . . . . . . . . . . . . . . . 17
⊢
(〈〈𝑔,
ℎ〉, 𝑖〉𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
209 | 206, 208 | bitrdi 290 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉 → (𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))) |
210 | 209 | notbid 321 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉 → (¬ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))) |
211 | 205, 210 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) → ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))))) |
212 | 203, 211 | mpbiri 261 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉)) |
213 | 212 | com12 32 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉 → ¬ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉)) |
214 | 213 | exlimdv 1940 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑖 𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉 → ¬ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉)) |
215 | 214 | exlimdvv 1941 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑔∃ℎ∃𝑖 𝑞 = 〈〈𝑔, ℎ〉, 𝑖〉 → ¬ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉)) |
216 | 107, 215 | mpd 15 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉) |
217 | 216 | ralrimiva 3096 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉) |
218 | | breq2 5034 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (𝑞𝑈𝑝 ↔ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉)) |
219 | 218 | notbid 321 |
. . . . . . . . . 10
⊢ (𝑝 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (¬ 𝑞𝑈𝑝 ↔ ¬ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉)) |
220 | 219 | ralbidv 3109 |
. . . . . . . . 9
⊢ (𝑝 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝 ↔ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉)) |
221 | 220 | rspcev 3526 |
. . . . . . . 8
⊢
((〈〈𝑎,
𝑏〉, 𝑐〉 ∈ 𝑠 ∧ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝) |
222 | 103, 217,
221 | syl2anc 587 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝) |
223 | 98, 222 | rexlimddv 3201 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝) |
224 | 67, 223 | rexlimddv 3201 |
. . . . 5
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝) |
225 | 40, 224 | rexlimddv 3201 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝) |
226 | 225 | ex 416 |
. . 3
⊢ (𝜑 → ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)) |
227 | 226 | alrimiv 1934 |
. 2
⊢ (𝜑 → ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)) |
228 | | df-fr 5483 |
. 2
⊢ (𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ↔ ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)) |
229 | 227, 228 | sylibr 237 |
1
⊢ (𝜑 → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶)) |