Step | Hyp | Ref
| Expression |
1 | | frxp3.1 |
. . . . . . 7
⊢ (𝜑 → 𝑅 Fr 𝐴) |
2 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑅 Fr 𝐴) |
3 | | dmss 5858 |
. . . . . . . . . 10
⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶)) |
4 | 3 | ad2antrl 726 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶)) |
5 | | dmxpss 6123 |
. . . . . . . . 9
⊢ dom
((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵) |
6 | 4, 5 | sstrdi 3956 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ (𝐴 × 𝐵)) |
7 | | dmss 5858 |
. . . . . . . 8
⊢ (dom
𝑠 ⊆ (𝐴 × 𝐵) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵)) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵)) |
9 | | dmxpss 6123 |
. . . . . . 7
⊢ dom
(𝐴 × 𝐵) ⊆ 𝐴 |
10 | 8, 9 | sstrdi 3956 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ 𝐴) |
11 | | vex 3449 |
. . . . . . . . 9
⊢ 𝑠 ∈ V |
12 | 11 | dmex 7848 |
. . . . . . . 8
⊢ dom 𝑠 ∈ V |
13 | 12 | dmex 7848 |
. . . . . . 7
⊢ dom dom
𝑠 ∈ V |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ∈ V) |
15 | | relxp 5651 |
. . . . . . . . . . . . 13
⊢ Rel
((𝐴 × 𝐵) × 𝐶) |
16 | | relss 5737 |
. . . . . . . . . . . . 13
⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → (Rel ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠)) |
17 | 15, 16 | mpi 20 |
. . . . . . . . . . . 12
⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠) |
18 | 17 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → Rel 𝑠) |
19 | | reldm0 5883 |
. . . . . . . . . . 11
⊢ (Rel
𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅)) |
21 | | relxp 5651 |
. . . . . . . . . . . . . 14
⊢ Rel
(𝐴 × 𝐵) |
22 | | relss 5737 |
. . . . . . . . . . . . . 14
⊢ (dom
((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel dom ((𝐴 × 𝐵) × 𝐶))) |
23 | 5, 21, 22 | mp2 9 |
. . . . . . . . . . . . 13
⊢ Rel dom
((𝐴 × 𝐵) × 𝐶) |
24 | | relss 5737 |
. . . . . . . . . . . . 13
⊢ (dom
𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶) → (Rel dom ((𝐴 × 𝐵) × 𝐶) → Rel dom 𝑠)) |
25 | 3, 23, 24 | mpisyl 21 |
. . . . . . . . . . . 12
⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → Rel dom 𝑠) |
26 | 25 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → Rel dom 𝑠) |
27 | | reldm0 5883 |
. . . . . . . . . . 11
⊢ (Rel dom
𝑠 → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅)) |
29 | 20, 28 | bitrd 278 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 = ∅ ↔ dom dom 𝑠 = ∅)) |
30 | 29 | necon3bid 2988 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅)) |
31 | 30 | biimpa 477 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) ∧ 𝑠 ≠ ∅) → dom dom 𝑠 ≠ ∅) |
32 | 31 | anasss 467 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ≠ ∅) |
33 | 2, 10, 14, 32 | frd 5592 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎) |
34 | | frxp3.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 Fr 𝐵) |
35 | 34 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑆 Fr 𝐵) |
36 | | imassrn 6024 |
. . . . . . . . 9
⊢ (dom
𝑠 “ {𝑎}) ⊆ ran dom 𝑠 |
37 | | rnss 5894 |
. . . . . . . . . . 11
⊢ (dom
𝑠 ⊆ (𝐴 × 𝐵) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵)) |
38 | 6, 37 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵)) |
39 | | rnxpss 6124 |
. . . . . . . . . 10
⊢ ran
(𝐴 × 𝐵) ⊆ 𝐵 |
40 | 38, 39 | sstrdi 3956 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ 𝐵) |
41 | 36, 40 | sstrid 3955 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 “ {𝑎}) ⊆ 𝐵) |
42 | 41 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ⊆ 𝐵) |
43 | 12 | imaex 7853 |
. . . . . . . 8
⊢ (dom
𝑠 “ {𝑎}) ∈ V |
44 | 43 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ∈ V) |
45 | | imadisj 6032 |
. . . . . . . . . . 11
⊢ ((dom
𝑠 “ {𝑎}) = ∅ ↔ (dom dom
𝑠 ∩ {𝑎}) = ∅) |
46 | | disjsn 4672 |
. . . . . . . . . . 11
⊢ ((dom dom
𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠) |
47 | 45, 46 | bitri 274 |
. . . . . . . . . 10
⊢ ((dom
𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠) |
48 | 47 | necon2abii 2994 |
. . . . . . . . 9
⊢ (𝑎 ∈ dom dom 𝑠 ↔ (dom 𝑠 “ {𝑎}) ≠ ∅) |
49 | 48 | biimpi 215 |
. . . . . . . 8
⊢ (𝑎 ∈ dom dom 𝑠 → (dom 𝑠 “ {𝑎}) ≠ ∅) |
50 | 49 | ad2antrl 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ≠ ∅) |
51 | 35, 42, 44, 50 | frd 5592 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏) |
52 | | frxp3.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 Fr 𝐶) |
53 | 52 | ad3antrrr 728 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 𝑇 Fr 𝐶) |
54 | | imassrn 6024 |
. . . . . . . . . 10
⊢ (𝑠 “ {〈𝑎, 𝑏〉}) ⊆ ran 𝑠 |
55 | | rnss 5894 |
. . . . . . . . . . . 12
⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶)) |
56 | 55 | ad2antrl 726 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶)) |
57 | | rnxpss 6124 |
. . . . . . . . . . 11
⊢ ran
((𝐴 × 𝐵) × 𝐶) ⊆ 𝐶 |
58 | 56, 57 | sstrdi 3956 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ 𝐶) |
59 | 54, 58 | sstrid 3955 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 “ {〈𝑎, 𝑏〉}) ⊆ 𝐶) |
60 | 59 | ad2antrr 724 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {〈𝑎, 𝑏〉}) ⊆ 𝐶) |
61 | 11 | imaex 7853 |
. . . . . . . . 9
⊢ (𝑠 “ {〈𝑎, 𝑏〉}) ∈ V |
62 | 61 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {〈𝑎, 𝑏〉}) ∈ V) |
63 | | simprl 769 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 𝑏 ∈ (dom 𝑠 “ {𝑎})) |
64 | | vex 3449 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
65 | | vex 3449 |
. . . . . . . . . . 11
⊢ 𝑏 ∈ V |
66 | 64, 65 | elimasn 6041 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ↔ 〈𝑎, 𝑏〉 ∈ dom 𝑠) |
67 | 63, 66 | sylib 217 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 〈𝑎, 𝑏〉 ∈ dom 𝑠) |
68 | | imadisj 6032 |
. . . . . . . . . . 11
⊢ ((𝑠 “ {〈𝑎, 𝑏〉}) = ∅ ↔ (dom 𝑠 ∩ {〈𝑎, 𝑏〉}) = ∅) |
69 | | disjsn 4672 |
. . . . . . . . . . 11
⊢ ((dom
𝑠 ∩ {〈𝑎, 𝑏〉}) = ∅ ↔ ¬ 〈𝑎, 𝑏〉 ∈ dom 𝑠) |
70 | 68, 69 | bitri 274 |
. . . . . . . . . 10
⊢ ((𝑠 “ {〈𝑎, 𝑏〉}) = ∅ ↔ ¬ 〈𝑎, 𝑏〉 ∈ dom 𝑠) |
71 | 70 | necon2abii 2994 |
. . . . . . . . 9
⊢
(〈𝑎, 𝑏〉 ∈ dom 𝑠 ↔ (𝑠 “ {〈𝑎, 𝑏〉}) ≠ ∅) |
72 | 67, 71 | sylib 217 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {〈𝑎, 𝑏〉}) ≠ ∅) |
73 | 53, 60, 62, 72 | frd 5592 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉})∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐) |
74 | | df-ot 4595 |
. . . . . . . . 9
⊢
〈𝑎, 𝑏, 𝑐〉 = 〈〈𝑎, 𝑏〉, 𝑐〉 |
75 | | simprl 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → 𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉})) |
76 | | opex 5421 |
. . . . . . . . . . 11
⊢
〈𝑎, 𝑏〉 ∈ V |
77 | | vex 3449 |
. . . . . . . . . . 11
⊢ 𝑐 ∈ V |
78 | 76, 77 | elimasn 6041 |
. . . . . . . . . 10
⊢ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ↔ 〈〈𝑎, 𝑏〉, 𝑐〉 ∈ 𝑠) |
79 | 75, 78 | sylib 217 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → 〈〈𝑎, 𝑏〉, 𝑐〉 ∈ 𝑠) |
80 | 74, 79 | eqeltrid 2842 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → 〈𝑎, 𝑏, 𝑐〉 ∈ 𝑠) |
81 | | simplrl 775 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) |
82 | 81 | ad2antrr 724 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) |
83 | | el2xpss 7969 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ 𝑠 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → ∃𝑔∃ℎ∃𝑖 𝑞 = 〈𝑔, ℎ, 𝑖〉) |
84 | 83 | ancoms 459 |
. . . . . . . . . . 11
⊢ ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ 𝑠) → ∃𝑔∃ℎ∃𝑖 𝑞 = 〈𝑔, ℎ, 𝑖〉) |
85 | 82, 84 | sylan 580 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ∃𝑔∃ℎ∃𝑖 𝑞 = 〈𝑔, ℎ, 𝑖〉) |
86 | | df-ne 2944 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ≠ 𝑐 ↔ ¬ 𝑖 = 𝑐) |
87 | 86 | con2bii 357 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = 𝑐 ↔ ¬ 𝑖 ≠ 𝑐) |
88 | 87 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = 𝑐 → ¬ 𝑖 ≠ 𝑐) |
89 | 88 | intnand 489 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = 𝑐 → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)) |
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)) |
91 | | breq1 5108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = 𝑖 → (𝑓𝑇𝑐 ↔ 𝑖𝑇𝑐)) |
92 | 91 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑖 → (¬ 𝑓𝑇𝑐 ↔ ¬ 𝑖𝑇𝑐)) |
93 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) → ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐) |
94 | 93 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐) |
95 | | df-ot 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
〈𝑎, 𝑏, 𝑖〉 = 〈〈𝑎, 𝑏〉, 𝑖〉 |
96 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) |
97 | 95, 96 | eqeltrrid 2843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) |
98 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑖 ∈ V |
99 | 76, 98 | elimasn 6041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ↔ 〈〈𝑎, 𝑏〉, 𝑖〉 ∈ 𝑠) |
100 | 97, 99 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 𝑖 ∈ (𝑠 “ {〈𝑎, 𝑏〉})) |
101 | 92, 94, 100 | rspcdva 3582 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ 𝑖𝑇𝑐) |
102 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐) |
103 | 102 | neneqd 2948 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ 𝑖 = 𝑐) |
104 | | ioran 982 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
(𝑖𝑇𝑐 ∨ 𝑖 = 𝑐) ↔ (¬ 𝑖𝑇𝑐 ∧ ¬ 𝑖 = 𝑐)) |
105 | 101, 103,
104 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) |
106 | 105 | intn3an3d 1481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐))) |
107 | 106 | intnanrd 490 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)) |
108 | 90, 107 | pm2.61dane 3032 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)) |
109 | | oteq2 4840 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ = 𝑏 → 〈𝑎, ℎ, 𝑖〉 = 〈𝑎, 𝑏, 𝑖〉) |
110 | 109 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = 𝑏 → (〈𝑎, ℎ, 𝑖〉 ∈ 𝑠 ↔ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠)) |
111 | 110 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠))) |
112 | | neeq1 3006 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ = 𝑏 → (ℎ ≠ 𝑏 ↔ 𝑏 ≠ 𝑏)) |
113 | 112 | orbi1d 915 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ = 𝑏 → ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
114 | | neirr 2952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ¬
𝑏 ≠ 𝑏 |
115 | | orel1 887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝑏 ≠ 𝑏 → ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐)) |
116 | 114, 115 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐) |
117 | | olc 866 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ≠ 𝑐 → (𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) |
118 | 116, 117 | impbii 208 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ 𝑖 ≠ 𝑐) |
119 | 113, 118 | bitrdi 286 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ = 𝑏 → ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ 𝑖 ≠ 𝑐)) |
120 | 119 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = 𝑏 → ((((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))) |
121 | 120 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = 𝑏 → (¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))) |
122 | 111, 121 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = 𝑏 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, 𝑏, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)))) |
123 | 108, 122 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
124 | 123 | impcom 408 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ = 𝑏) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
125 | | breq1 5108 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑒 = ℎ → (𝑒𝑆𝑏 ↔ ℎ𝑆𝑏)) |
126 | 125 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑒 = ℎ → (¬ 𝑒𝑆𝑏 ↔ ¬ ℎ𝑆𝑏)) |
127 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏) |
128 | 127 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏) |
129 | | df-ot 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
〈𝑎, ℎ, 𝑖〉 = 〈〈𝑎, ℎ〉, 𝑖〉 |
130 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) |
131 | 129, 130 | eqeltrrid 2843 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → 〈〈𝑎, ℎ〉, 𝑖〉 ∈ 𝑠) |
132 | | opex 5421 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
〈𝑎, ℎ〉 ∈ V |
133 | 132, 98 | opeldm 5863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(〈〈𝑎,
ℎ〉, 𝑖〉 ∈ 𝑠 → 〈𝑎, ℎ〉 ∈ dom 𝑠) |
134 | 131, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → 〈𝑎, ℎ〉 ∈ dom 𝑠) |
135 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ℎ ∈ V |
136 | 64, 135 | elimasn 6041 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ ∈ (dom 𝑠 “ {𝑎}) ↔ 〈𝑎, ℎ〉 ∈ dom 𝑠) |
137 | 134, 136 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ℎ ∈ (dom 𝑠 “ {𝑎})) |
138 | 126, 128,
137 | rspcdva 3582 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ℎ𝑆𝑏) |
139 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ℎ ≠ 𝑏) |
140 | 139 | neneqd 2948 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ℎ = 𝑏) |
141 | | ioran 982 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
(ℎ𝑆𝑏 ∨ ℎ = 𝑏) ↔ (¬ ℎ𝑆𝑏 ∧ ¬ ℎ = 𝑏)) |
142 | 138, 140,
141 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ (ℎ𝑆𝑏 ∨ ℎ = 𝑏)) |
143 | 142 | intn3an2d 1480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐))) |
144 | 143 | intnanrd 490 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
145 | 124, 144 | pm2.61dane 3032 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
146 | | oteq1 4839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑎 → 〈𝑔, ℎ, 𝑖〉 = 〈𝑎, ℎ, 𝑖〉) |
147 | 146 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑎 → (〈𝑔, ℎ, 𝑖〉 ∈ 𝑠 ↔ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠)) |
148 | 147 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠))) |
149 | | neeq1 3006 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 = 𝑎 → (𝑔 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎)) |
150 | | biidd 261 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 = 𝑎 → (ℎ ≠ 𝑏 ↔ ℎ ≠ 𝑏)) |
151 | | biidd 261 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 = 𝑎 → (𝑖 ≠ 𝑐 ↔ 𝑖 ≠ 𝑐)) |
152 | 149, 150,
151 | 3orbi123d 1435 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
153 | | 3orass 1090 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
154 | | neirr 2952 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ¬
𝑎 ≠ 𝑎 |
155 | | orel1 887 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑎 ≠ 𝑎 → ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) → (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
156 | 154, 155 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) → (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) |
157 | | olc 866 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
158 | 156, 157 | impbii 208 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) |
159 | 153, 158 | bitri 274 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) |
160 | 152, 159 | bitrdi 286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
161 | 160 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑎 → ((((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
162 | 161 | notbid 317 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑎 → (¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
163 | 148, 162 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑎 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑎, ℎ, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))) |
164 | 145, 163 | mpbiri 257 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
165 | 164 | impcom 408 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ∧ 𝑔 = 𝑎) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
166 | | breq1 5108 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 = 𝑔 → (𝑑𝑅𝑎 ↔ 𝑔𝑅𝑎)) |
167 | 166 | notbid 317 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = 𝑔 → (¬ 𝑑𝑅𝑎 ↔ ¬ 𝑔𝑅𝑎)) |
168 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎) |
169 | 168 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎) |
170 | | df-ot 4595 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
〈𝑔, ℎ, 𝑖〉 = 〈〈𝑔, ℎ〉, 𝑖〉 |
171 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) |
172 | 170, 171 | eqeltrrid 2843 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 〈〈𝑔, ℎ〉, 𝑖〉 ∈ 𝑠) |
173 | | opex 5421 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
〈𝑔, ℎ〉 ∈ V |
174 | 173, 98 | opeldm 5863 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈〈𝑔,
ℎ〉, 𝑖〉 ∈ 𝑠 → 〈𝑔, ℎ〉 ∈ dom 𝑠) |
175 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑔 ∈ V |
176 | 175, 135 | opeldm 5863 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈𝑔, ℎ〉 ∈ dom 𝑠 → 𝑔 ∈ dom dom 𝑠) |
177 | 172, 174,
176 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 𝑔 ∈ dom dom 𝑠) |
178 | 167, 169,
177 | rspcdva 3582 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ 𝑔𝑅𝑎) |
179 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 𝑔 ≠ 𝑎) |
180 | 179 | neneqd 2948 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ 𝑔 = 𝑎) |
181 | | ioran 982 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ↔ (¬ 𝑔𝑅𝑎 ∧ ¬ 𝑔 = 𝑎)) |
182 | 178, 180,
181 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ (𝑔𝑅𝑎 ∨ 𝑔 = 𝑎)) |
183 | 182 | intn3an1d 1479 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐))) |
184 | 183 | intnanrd 490 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
185 | 165, 184 | pm2.61dane 3032 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) |
186 | 185 | intn3an3d 1481 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) → ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
187 | | eleq1 2825 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 = 〈𝑔, ℎ, 𝑖〉 → (𝑞 ∈ 𝑠 ↔ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠)) |
188 | 187 | anbi2d 629 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 〈𝑔, ℎ, 𝑖〉 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠))) |
189 | | breq1 5108 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 = 〈𝑔, ℎ, 𝑖〉 → (𝑞𝑈〈𝑎, 𝑏, 𝑐〉 ↔ 〈𝑔, ℎ, 𝑖〉𝑈〈𝑎, 𝑏, 𝑐〉)) |
190 | | xpord3.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} |
191 | 190 | xpord3lem 8081 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑔, ℎ, 𝑖〉𝑈〈𝑎, 𝑏, 𝑐〉 ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))) |
192 | 189, 191 | bitrdi 286 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 = 〈𝑔, ℎ, 𝑖〉 → (𝑞𝑈〈𝑎, 𝑏, 𝑐〉 ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))) |
193 | 192 | notbid 317 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 〈𝑔, ℎ, 𝑖〉 → (¬ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉 ↔ ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))) |
194 | 188, 193 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 〈𝑔, ℎ, 𝑖〉 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 〈𝑔, ℎ, 𝑖〉 ∈ 𝑠) → ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))))) |
195 | 186, 194 | mpbiri 257 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 〈𝑔, ℎ, 𝑖〉 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉)) |
196 | 195 | com12 32 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (𝑞 = 〈𝑔, ℎ, 𝑖〉 → ¬ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉)) |
197 | 196 | exlimdv 1936 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑖 𝑞 = 〈𝑔, ℎ, 𝑖〉 → ¬ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉)) |
198 | 197 | exlimdvv 1937 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑔∃ℎ∃𝑖 𝑞 = 〈𝑔, ℎ, 𝑖〉 → ¬ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉)) |
199 | 85, 198 | mpd 15 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉) |
200 | 199 | ralrimiva 3143 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉) |
201 | | breq2 5109 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑎, 𝑏, 𝑐〉 → (𝑞𝑈𝑝 ↔ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉)) |
202 | 201 | notbid 317 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑎, 𝑏, 𝑐〉 → (¬ 𝑞𝑈𝑝 ↔ ¬ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉)) |
203 | 202 | ralbidv 3174 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑎, 𝑏, 𝑐〉 → (∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝 ↔ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉)) |
204 | 203 | rspcev 3581 |
. . . . . . . 8
⊢
((〈𝑎, 𝑏, 𝑐〉 ∈ 𝑠 ∧ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝) |
205 | 80, 200, 204 | syl2anc 584 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ∧ ∀𝑓 ∈ (𝑠 “ {〈𝑎, 𝑏〉}) ¬ 𝑓𝑇𝑐)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝) |
206 | 73, 205 | rexlimddv 3158 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝) |
207 | 51, 206 | rexlimddv 3158 |
. . . . 5
⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝) |
208 | 33, 207 | rexlimddv 3158 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝) |
209 | 208 | ex 413 |
. . 3
⊢ (𝜑 → ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)) |
210 | 209 | alrimiv 1930 |
. 2
⊢ (𝜑 → ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)) |
211 | | df-fr 5588 |
. 2
⊢ (𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ↔ ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)) |
212 | 210, 211 | sylibr 233 |
1
⊢ (𝜑 → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶)) |