Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frxp3 Structured version   Visualization version   GIF version

Theorem frxp3 33408
Description: Give foundedness over a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024.)
Hypotheses
Ref Expression
xpord3.1 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦))}
frxp3.1 (𝜑𝑅 Fr 𝐴)
frxp3.2 (𝜑𝑆 Fr 𝐵)
frxp3.3 (𝜑𝑇 Fr 𝐶)
Assertion
Ref Expression
frxp3 (𝜑𝑈 Fr ((𝐴 × 𝐵) × 𝐶))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑈(𝑥,𝑦)

Proof of Theorem frxp3
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 𝑝 𝑞 𝑠 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmss 5745 . . . . . . . . . 10 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
21ad2antrl 728 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
3 dmxpss 6003 . . . . . . . . 9 dom ((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵)
42, 3sstrdi 3889 . . . . . . . 8 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ (𝐴 × 𝐵))
5 dmss 5745 . . . . . . . 8 (dom 𝑠 ⊆ (𝐴 × 𝐵) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
64, 5syl 17 . . . . . . 7 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
7 dmxpss 6003 . . . . . . 7 dom (𝐴 × 𝐵) ⊆ 𝐴
86, 7sstrdi 3889 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠𝐴)
9 simprr 773 . . . . . . . 8 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑠 ≠ ∅)
10 simprl 771 . . . . . . . . . . 11 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
11 relxp 5543 . . . . . . . . . . 11 Rel ((𝐴 × 𝐵) × 𝐶)
12 relss 5627 . . . . . . . . . . 11 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → (Rel ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠))
1310, 11, 12mpisyl 21 . . . . . . . . . 10 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → Rel 𝑠)
14 reldm0 5771 . . . . . . . . . 10 (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1513, 14syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1615necon3bid 2978 . . . . . . . 8 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
179, 16mpbid 235 . . . . . . 7 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ≠ ∅)
18 relxp 5543 . . . . . . . . . 10 Rel (𝐴 × 𝐵)
19 relss 5627 . . . . . . . . . 10 (dom 𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel dom 𝑠))
204, 18, 19mpisyl 21 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → Rel dom 𝑠)
21 reldm0 5771 . . . . . . . . 9 (Rel dom 𝑠 → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
2220, 21syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
2322necon3bid 2978 . . . . . . 7 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅))
2417, 23mpbid 235 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ≠ ∅)
25 frxp3.1 . . . . . . . . 9 (𝜑𝑅 Fr 𝐴)
26 df-fr 5483 . . . . . . . . 9 (𝑅 Fr 𝐴 ↔ ∀𝑔((𝑔𝐴𝑔 ≠ ∅) → ∃𝑎𝑔𝑑𝑔 ¬ 𝑑𝑅𝑎))
2725, 26sylib 221 . . . . . . . 8 (𝜑 → ∀𝑔((𝑔𝐴𝑔 ≠ ∅) → ∃𝑎𝑔𝑑𝑔 ¬ 𝑑𝑅𝑎))
2827adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∀𝑔((𝑔𝐴𝑔 ≠ ∅) → ∃𝑎𝑔𝑑𝑔 ¬ 𝑑𝑅𝑎))
29 vex 3402 . . . . . . . . . 10 𝑠 ∈ V
3029dmex 7642 . . . . . . . . 9 dom 𝑠 ∈ V
3130dmex 7642 . . . . . . . 8 dom dom 𝑠 ∈ V
32 sseq1 3902 . . . . . . . . . 10 (𝑔 = dom dom 𝑠 → (𝑔𝐴 ↔ dom dom 𝑠𝐴))
33 neeq1 2996 . . . . . . . . . 10 (𝑔 = dom dom 𝑠 → (𝑔 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅))
3432, 33anbi12d 634 . . . . . . . . 9 (𝑔 = dom dom 𝑠 → ((𝑔𝐴𝑔 ≠ ∅) ↔ (dom dom 𝑠𝐴 ∧ dom dom 𝑠 ≠ ∅)))
35 raleq 3310 . . . . . . . . . 10 (𝑔 = dom dom 𝑠 → (∀𝑑𝑔 ¬ 𝑑𝑅𝑎 ↔ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎))
3635rexeqbi1dv 3309 . . . . . . . . 9 (𝑔 = dom dom 𝑠 → (∃𝑎𝑔𝑑𝑔 ¬ 𝑑𝑅𝑎 ↔ ∃𝑎 ∈ dom dom 𝑠𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎))
3734, 36imbi12d 348 . . . . . . . 8 (𝑔 = dom dom 𝑠 → (((𝑔𝐴𝑔 ≠ ∅) → ∃𝑎𝑔𝑑𝑔 ¬ 𝑑𝑅𝑎) ↔ ((dom dom 𝑠𝐴 ∧ dom dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom dom 𝑠𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)))
3831, 37spcv 3509 . . . . . . 7 (∀𝑔((𝑔𝐴𝑔 ≠ ∅) → ∃𝑎𝑔𝑑𝑔 ¬ 𝑑𝑅𝑎) → ((dom dom 𝑠𝐴 ∧ dom dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom dom 𝑠𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎))
3928, 38syl 17 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ((dom dom 𝑠𝐴 ∧ dom dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom dom 𝑠𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎))
408, 24, 39mp2and 699 . . . . 5 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom dom 𝑠𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
41 imassrn 5914 . . . . . . . 8 (dom 𝑠 “ {𝑎}) ⊆ ran dom 𝑠
42 rnss 5782 . . . . . . . . . . 11 (dom 𝑠 ⊆ (𝐴 × 𝐵) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
434, 42syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
44 rnxpss 6004 . . . . . . . . . 10 ran (𝐴 × 𝐵) ⊆ 𝐵
4543, 44sstrdi 3889 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠𝐵)
4645adantr 484 . . . . . . . 8 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ran dom 𝑠𝐵)
4741, 46sstrid 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 𝑠)
5149, 50bitri 278 . . . . . . . . 9 ((dom 𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠)
5251necon2abii 2984 . . . . . . . 8 (𝑎 ∈ dom dom 𝑠 ↔ (dom 𝑠 “ {𝑎}) ≠ ∅)
5348, 52sylib 221 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ≠ ∅)
54 frxp3.2 . . . . . . . . . 10 (𝜑𝑆 Fr 𝐵)
55 df-fr 5483 . . . . . . . . . 10 (𝑆 Fr 𝐵 ↔ ∀𝑔((𝑔𝐵𝑔 ≠ ∅) → ∃𝑏𝑔𝑒𝑔 ¬ 𝑒𝑆𝑏))
5654, 55sylib 221 . . . . . . . . 9 (𝜑 → ∀𝑔((𝑔𝐵𝑔 ≠ ∅) → ∃𝑏𝑔𝑒𝑔 ¬ 𝑒𝑆𝑏))
5730imaex 7647 . . . . . . . . . 10 (dom 𝑠 “ {𝑎}) ∈ V
58 sseq1 3902 . . . . . . . . . . . 12 (𝑔 = (dom 𝑠 “ {𝑎}) → (𝑔𝐵 ↔ (dom 𝑠 “ {𝑎}) ⊆ 𝐵))
59 neeq1 2996 . . . . . . . . . . . 12 (𝑔 = (dom 𝑠 “ {𝑎}) → (𝑔 ≠ ∅ ↔ (dom 𝑠 “ {𝑎}) ≠ ∅))
6058, 59anbi12d 634 . . . . . . . . . . 11 (𝑔 = (dom 𝑠 “ {𝑎}) → ((𝑔𝐵𝑔 ≠ ∅) ↔ ((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅)))
61 raleq 3310 . . . . . . . . . . . 12 (𝑔 = (dom 𝑠 “ {𝑎}) → (∀𝑒𝑔 ¬ 𝑒𝑆𝑏 ↔ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
6261rexeqbi1dv 3309 . . . . . . . . . . 11 (𝑔 = (dom 𝑠 “ {𝑎}) → (∃𝑏𝑔𝑒𝑔 ¬ 𝑒𝑆𝑏 ↔ ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
6360, 62imbi12d 348 . . . . . . . . . 10 (𝑔 = (dom 𝑠 “ {𝑎}) → (((𝑔𝐵𝑔 ≠ ∅) → ∃𝑏𝑔𝑒𝑔 ¬ 𝑒𝑆𝑏) ↔ (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)))
6457, 63spcv 3509 . . . . . . . . 9 (∀𝑔((𝑔𝐵𝑔 ≠ ∅) → ∃𝑏𝑔𝑒𝑔 ¬ 𝑒𝑆𝑏) → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
6556, 64syl 17 . . . . . . . 8 (𝜑 → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
6665ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
6747, 53, 66mp2and 699 . . . . . 6 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
68 imassrn 5914 . . . . . . . . . 10 (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ ran 𝑠
69 rnss 5782 . . . . . . . . . . . 12 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
7069ad2antrl 728 . . . . . . . . . . 11 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
71 rnxpss 6004 . . . . . . . . . . 11 ran ((𝐴 × 𝐵) × 𝐶) ⊆ 𝐶
7270, 71sstrdi 3889 . . . . . . . . . 10 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠𝐶)
7368, 72sstrid 3888 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶)
7473ad2antrr 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
7876, 77elimasn 5928 . . . . . . . . . 10 (𝑏 ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
7975, 78sylib 221 . . . . . . . . 9 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
80 imadisj 5922 . . . . . . . . . . 11 ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ (dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅)
81 disjsn 4602 . . . . . . . . . . 11 ((dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
8280, 81bitri 278 . . . . . . . . . 10 ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
8382necon2abii 2984 . . . . . . . . 9 (⟨𝑎, 𝑏⟩ ∈ dom 𝑠 ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
8479, 83sylib 221 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
85 frxp3.3 . . . . . . . . . . 11 (𝜑𝑇 Fr 𝐶)
86 df-fr 5483 . . . . . . . . . . 11 (𝑇 Fr 𝐶 ↔ ∀𝑔((𝑔𝐶𝑔 ≠ ∅) → ∃𝑐𝑔𝑓𝑔 ¬ 𝑓𝑇𝑐))
8785, 86sylib 221 . . . . . . . . . 10 (𝜑 → ∀𝑔((𝑔𝐶𝑔 ≠ ∅) → ∃𝑐𝑔𝑓𝑔 ¬ 𝑓𝑇𝑐))
8829imaex 7647 . . . . . . . . . . 11 (𝑠 “ {⟨𝑎, 𝑏⟩}) ∈ V
89 sseq1 3902 . . . . . . . . . . . . 13 (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (𝑔𝐶 ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶))
90 neeq1 2996 . . . . . . . . . . . . 13 (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (𝑔 ≠ ∅ ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅))
9189, 90anbi12d 634 . . . . . . . . . . . 12 (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → ((𝑔𝐶𝑔 ≠ ∅) ↔ ((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)))
92 raleq 3310 . . . . . . . . . . . . 13 (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (∀𝑓𝑔 ¬ 𝑓𝑇𝑐 ↔ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
9392rexeqbi1dv 3309 . . . . . . . . . . . 12 (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (∃𝑐𝑔𝑓𝑔 ¬ 𝑓𝑇𝑐 ↔ ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
9491, 93imbi12d 348 . . . . . . . . . . 11 (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (((𝑔𝐶𝑔 ≠ ∅) → ∃𝑐𝑔𝑓𝑔 ¬ 𝑓𝑇𝑐) ↔ (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)))
9588, 94spcv 3509 . . . . . . . . . 10 (∀𝑔((𝑔𝐶𝑔 ≠ ∅) → ∃𝑐𝑔𝑓𝑔 ¬ 𝑓𝑇𝑐) → (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
9687, 95syl 17 . . . . . . . . 9 (𝜑 → (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
9796ad3antrrr 730 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
9874, 84, 97mp2and 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
102100, 101elimasn 5928 . . . . . . . . 9 (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
10399, 102sylib 221 . . . . . . . 8 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
104 simplrl 777 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
105104ad2antrr 726 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
106 elxpxpss 33258 . . . . . . . . . . 11 ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑠) → ∃𝑔𝑖 𝑞 = ⟨⟨𝑔, ⟩, 𝑖⟩)
107105, 106sylan 583 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ∃𝑔𝑖 𝑞 = ⟨⟨𝑔, ⟩, 𝑖⟩)
108 df-ne 2935 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖𝑐 ↔ ¬ 𝑖 = 𝑐)
109108con2bii 361 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑐 ↔ ¬ 𝑖𝑐)
110109biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑐 → ¬ 𝑖𝑐)
111110adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ 𝑖𝑐)
112111intnand 492 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))
113 breq1 5033 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑖 → (𝑓𝑇𝑐𝑖𝑇𝑐))
114113notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑖 → (¬ 𝑓𝑇𝑐 ↔ ¬ 𝑖𝑇𝑐))
115 simplrr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
116115adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
117 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
118 vex 3402 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑖 ∈ V
119100, 118elimasn 5928 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
120117, 119sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → 𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}))
121114, 116, 120rspcdva 3528 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ 𝑖𝑇𝑐)
122 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → 𝑖𝑐)
123122neneqd 2939 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ 𝑖 = 𝑐)
124 ioran 983 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝑖𝑇𝑐𝑖 = 𝑐) ↔ (¬ 𝑖𝑇𝑐 ∧ ¬ 𝑖 = 𝑐))
125121, 123, 124sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ (𝑖𝑇𝑐𝑖 = 𝑐))
126125intn3an3d 1482 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ ((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)))
127126intnanrd 493 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))
128112, 127pm2.61dane 3021 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))
129 opeq2 4761 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = 𝑏 → ⟨𝑎, ⟩ = ⟨𝑎, 𝑏⟩)
130129opeq1d 4767 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = 𝑏 → ⟨⟨𝑎, ⟩, 𝑖⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑖⟩)
131130eleq1d 2817 . . . . . . . . . . . . . . . . . . . . . . 23 ( = 𝑏 → (⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠 ↔ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠))
132131anbi2d 632 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)))
133 neeq1 2996 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( = 𝑏 → (𝑏𝑏𝑏))
134133orbi1d 916 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = 𝑏 → ((𝑏𝑖𝑐) ↔ (𝑏𝑏𝑖𝑐)))
135 neirr 2943 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ¬ 𝑏𝑏
136 orel1 888 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑏𝑏 → ((𝑏𝑏𝑖𝑐) → 𝑖𝑐))
137135, 136ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏𝑏𝑖𝑐) → 𝑖𝑐)
138 olc 867 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖𝑐 → (𝑏𝑏𝑖𝑐))
139137, 138impbii 212 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏𝑏𝑖𝑐) ↔ 𝑖𝑐)
140134, 139bitrdi 290 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = 𝑏 → ((𝑏𝑖𝑐) ↔ 𝑖𝑐))
141140anbi2d 632 . . . . . . . . . . . . . . . . . . . . . . 23 ( = 𝑏 → ((((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)) ↔ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐)))
142141notbid 321 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑏 → (¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)) ↔ ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐)))
143132, 142imbi12d 348 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑏 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))))
144128, 143mpbiri 261 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))))
145144impcom 411 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) ∧ = 𝑏) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))
146 breq1 5033 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = → (𝑒𝑆𝑏𝑆𝑏))
147146notbid 321 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = → (¬ 𝑒𝑆𝑏 ↔ ¬ 𝑆𝑏))
148 simplrr 778 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
149148ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
150 opex 5322 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎, ⟩ ∈ V
151150, 118opeldm 5750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑎, ⟩ ∈ dom 𝑠)
152151adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) → ⟨𝑎, ⟩ ∈ dom 𝑠)
153152adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ⟨𝑎, ⟩ ∈ dom 𝑠)
154 vex 3402 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∈ V
15576, 154elimasn 5928 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, ⟩ ∈ dom 𝑠)
156153, 155sylibr 237 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ∈ (dom 𝑠 “ {𝑎}))
157147, 149, 156rspcdva 3528 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ 𝑆𝑏)
158 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → 𝑏)
159158neneqd 2939 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ = 𝑏)
160 ioran 983 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑆𝑏 = 𝑏) ↔ (¬ 𝑆𝑏 ∧ ¬ = 𝑏))
161157, 159, 160sylanbrc 586 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ (𝑆𝑏 = 𝑏))
162161intn3an2d 1481 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ ((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)))
163162intnanrd 493 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))
164145, 163pm2.61dane 3021 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))
165 opeq1 4759 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑎 → ⟨𝑔, ⟩ = ⟨𝑎, ⟩)
166165opeq1d 4767 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑎 → ⟨⟨𝑔, ⟩, 𝑖⟩ = ⟨⟨𝑎, ⟩, 𝑖⟩)
167166eleq1d 2817 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑎 → (⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠 ↔ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠))
168167anbi2d 632 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠)))
169 3orass 1091 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔𝑎𝑏𝑖𝑐) ↔ (𝑔𝑎 ∨ (𝑏𝑖𝑐)))
170 neeq1 2996 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 = 𝑎 → (𝑔𝑎𝑎𝑎))
171170orbi1d 916 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝑎 → ((𝑔𝑎 ∨ (𝑏𝑖𝑐)) ↔ (𝑎𝑎 ∨ (𝑏𝑖𝑐))))
172169, 171syl5bb 286 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑎 → ((𝑔𝑎𝑏𝑖𝑐) ↔ (𝑎𝑎 ∨ (𝑏𝑖𝑐))))
173 neirr 2943 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ 𝑎𝑎
174 orel1 888 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑎𝑎 → ((𝑎𝑎 ∨ (𝑏𝑖𝑐)) → (𝑏𝑖𝑐)))
175173, 174ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑎 ∨ (𝑏𝑖𝑐)) → (𝑏𝑖𝑐))
176 olc 867 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑖𝑐) → (𝑎𝑎 ∨ (𝑏𝑖𝑐)))
177175, 176impbii 212 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑎 ∨ (𝑏𝑖𝑐)) ↔ (𝑏𝑖𝑐))
178172, 177bitrdi 290 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑎 → ((𝑔𝑎𝑏𝑖𝑐) ↔ (𝑏𝑖𝑐)))
179178anbi2d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑎 → ((((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)) ↔ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))))
180179notbid 321 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑎 → (¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)) ↔ ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))))
181168, 180imbi12d 348 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑎 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))))
182164, 181mpbiri 261 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))
183182impcom 411 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 = 𝑎) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))
184 breq1 5033 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑔 → (𝑑𝑅𝑎𝑔𝑅𝑎))
185184notbid 321 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑔 → (¬ 𝑑𝑅𝑎 ↔ ¬ 𝑔𝑅𝑎))
186 simplrr 778 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
187186ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
188 opex 5322 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑔, ⟩ ∈ V
189188, 118opeldm 5750 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑔, ⟩ ∈ dom 𝑠)
190189adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) → ⟨𝑔, ⟩ ∈ dom 𝑠)
191 vex 3402 . . . . . . . . . . . . . . . . . . . . . . 23 𝑔 ∈ V
192191, 154opeldm 5750 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑔, ⟩ ∈ dom 𝑠𝑔 ∈ dom dom 𝑠)
193190, 192syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) → 𝑔 ∈ dom dom 𝑠)
194193adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → 𝑔 ∈ dom dom 𝑠)
195185, 187, 194rspcdva 3528 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ 𝑔𝑅𝑎)
196 simpr 488 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → 𝑔𝑎)
197196neneqd 2939 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ 𝑔 = 𝑎)
198 ioran 983 . . . . . . . . . . . . . . . . . . 19 (¬ (𝑔𝑅𝑎𝑔 = 𝑎) ↔ (¬ 𝑔𝑅𝑎 ∧ ¬ 𝑔 = 𝑎))
199195, 197, 198sylanbrc 586 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ (𝑔𝑅𝑎𝑔 = 𝑎))
200199intn3an1d 1480 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ ((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)))
201200intnanrd 493 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))
202183, 201pm2.61dane 3021 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))
203202intn3an3d 1482 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))
204 eleq1 2820 . . . . . . . . . . . . . . . 16 (𝑞 = ⟨⟨𝑔, ⟩, 𝑖⟩ → (𝑞𝑠 ↔ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠))
205204anbi2d 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𝑦))) ∧ 𝑥𝑦))}
208207xpord3lem 33406 . . . . . . . . . . . . . . . . 17 (⟨⟨𝑔, ⟩, 𝑖𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))
209206, 208bitrdi 290 . . . . . . . . . . . . . . . 16 (𝑞 = ⟨⟨𝑔, ⟩, 𝑖⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))))
210209notbid 321 . . . . . . . . . . . . . . 15 (𝑞 = ⟨⟨𝑔, ⟩, 𝑖⟩ → (¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ¬ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))))
211205, 210imbi12d 348 . . . . . . . . . . . . . 14 (𝑞 = ⟨⟨𝑔, ⟩, 𝑖⟩ → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))))
212203, 211mpbiri 261 . . . . . . . . . . . . 13 (𝑞 = ⟨⟨𝑔, ⟩, 𝑖⟩ → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
213212com12 32 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → (𝑞 = ⟨⟨𝑔, ⟩, 𝑖⟩ → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
214213exlimdv 1940 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → (∃𝑖 𝑞 = ⟨⟨𝑔, ⟩, 𝑖⟩ → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
215214exlimdvv 1941 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → (∃𝑔𝑖 𝑞 = ⟨⟨𝑔, ⟩, 𝑖⟩ → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
216107, 215mpd 15 . . . . . . . . 9 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩)
217216ralrimiva 3096 . . . . . . . 8 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑞𝑠 ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩)
218 breq2 5034 . . . . . . . . . . 11 (𝑝 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (𝑞𝑈𝑝𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
219218notbid 321 . . . . . . . . . 10 (𝑝 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (¬ 𝑞𝑈𝑝 ↔ ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
220219ralbidv 3109 . . . . . . . . 9 (𝑝 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (∀𝑞𝑠 ¬ 𝑞𝑈𝑝 ↔ ∀𝑞𝑠 ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
221220rspcev 3526 . . . . . . . 8 ((⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠 ∧ ∀𝑞𝑠 ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
222103, 217, 221syl2anc 587 . . . . . . 7 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
22398, 222rexlimddv 3201 . . . . . 6 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
22467, 223rexlimddv 3201 . . . . 5 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
22540, 224rexlimddv 3201 . . . 4 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
226225ex 416 . . 3 (𝜑 → ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝))
227226alrimiv 1934 . 2 (𝜑 → ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝))
228 df-fr 5483 . 2 (𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ↔ ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝))
229227, 228sylibr 237 1 (𝜑𝑈 Fr ((𝐴 × 𝐵) × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846  w3o 1087  w3a 1088  wal 1540   = wceq 1542  wex 1786  wcel 2114  wne 2934  wral 3053  wrex 3054  cin 3842  wss 3843  c0 4211  {csn 4516  cop 4522   class class class wbr 5030  {copab 5092   Fr wfr 5480   × cxp 5523  dom cdm 5525  ran crn 5526  cima 5528  Rel wrel 5530  cfv 6339  1st c1st 7712  2nd c2nd 7713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296  ax-un 7479
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-fr 5483  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fv 6347  df-1st 7714  df-2nd 7715
This theorem is referenced by:  xpord3ind  33411  no3indslem  33752
  Copyright terms: Public domain W3C validator