MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frxp3 Structured version   Visualization version   GIF version

Theorem frxp3 8083
Description: Give well-foundedness over a triple Cartesian 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 frxp3.1 . . . . . . 7 (𝜑𝑅 Fr 𝐴)
21adantr 481 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑅 Fr 𝐴)
3 dmss 5858 . . . . . . . . . 10 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
43ad2antrl 726 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
5 dmxpss 6123 . . . . . . . . 9 dom ((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵)
64, 5sstrdi 3956 . . . . . . . 8 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ (𝐴 × 𝐵))
7 dmss 5858 . . . . . . . 8 (dom 𝑠 ⊆ (𝐴 × 𝐵) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
86, 7syl 17 . . . . . . 7 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
9 dmxpss 6123 . . . . . . 7 dom (𝐴 × 𝐵) ⊆ 𝐴
108, 9sstrdi 3956 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠𝐴)
11 vex 3449 . . . . . . . . 9 𝑠 ∈ V
1211dmex 7848 . . . . . . . 8 dom 𝑠 ∈ V
1312dmex 7848 . . . . . . 7 dom dom 𝑠 ∈ V
1413a1i 11 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ∈ V)
15 relxp 5651 . . . . . . . . . . . . 13 Rel ((𝐴 × 𝐵) × 𝐶)
16 relss 5737 . . . . . . . . . . . . 13 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → (Rel ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠))
1715, 16mpi 20 . . . . . . . . . . . 12 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠)
1817adantl 482 . . . . . . . . . . 11 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → Rel 𝑠)
19 reldm0 5883 . . . . . . . . . . 11 (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
2018, 19syl 17 . . . . . . . . . 10 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
21 relxp 5651 . . . . . . . . . . . . . 14 Rel (𝐴 × 𝐵)
22 relss 5737 . . . . . . . . . . . . . 14 (dom ((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel dom ((𝐴 × 𝐵) × 𝐶)))
235, 21, 22mp2 9 . . . . . . . . . . . . 13 Rel dom ((𝐴 × 𝐵) × 𝐶)
24 relss 5737 . . . . . . . . . . . . 13 (dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶) → (Rel dom ((𝐴 × 𝐵) × 𝐶) → Rel dom 𝑠))
253, 23, 24mpisyl 21 . . . . . . . . . . . 12 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → Rel dom 𝑠)
2625adantl 482 . . . . . . . . . . 11 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → Rel dom 𝑠)
27 reldm0 5883 . . . . . . . . . . 11 (Rel dom 𝑠 → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
2826, 27syl 17 . . . . . . . . . 10 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
2920, 28bitrd 278 . . . . . . . . 9 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
3029necon3bid 2988 . . . . . . . 8 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅))
3130biimpa 477 . . . . . . 7 (((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) ∧ 𝑠 ≠ ∅) → dom dom 𝑠 ≠ ∅)
3231anasss 467 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ≠ ∅)
332, 10, 14, 32frd 5592 . . . . 5 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom dom 𝑠𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
34 frxp3.2 . . . . . . . 8 (𝜑𝑆 Fr 𝐵)
3534ad2antrr 724 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑆 Fr 𝐵)
36 imassrn 6024 . . . . . . . . 9 (dom 𝑠 “ {𝑎}) ⊆ ran dom 𝑠
37 rnss 5894 . . . . . . . . . . 11 (dom 𝑠 ⊆ (𝐴 × 𝐵) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
386, 37syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
39 rnxpss 6124 . . . . . . . . . 10 ran (𝐴 × 𝐵) ⊆ 𝐵
4038, 39sstrdi 3956 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠𝐵)
4136, 40sstrid 3955 . . . . . . . 8 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 “ {𝑎}) ⊆ 𝐵)
4241adantr 481 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ⊆ 𝐵)
4312imaex 7853 . . . . . . . 8 (dom 𝑠 “ {𝑎}) ∈ V
4443a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ∈ V)
45 imadisj 6032 . . . . . . . . . . 11 ((dom 𝑠 “ {𝑎}) = ∅ ↔ (dom dom 𝑠 ∩ {𝑎}) = ∅)
46 disjsn 4672 . . . . . . . . . . 11 ((dom dom 𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠)
4745, 46bitri 274 . . . . . . . . . 10 ((dom 𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠)
4847necon2abii 2994 . . . . . . . . 9 (𝑎 ∈ dom dom 𝑠 ↔ (dom 𝑠 “ {𝑎}) ≠ ∅)
4948biimpi 215 . . . . . . . 8 (𝑎 ∈ dom dom 𝑠 → (dom 𝑠 “ {𝑎}) ≠ ∅)
5049ad2antrl 726 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ≠ ∅)
5135, 42, 44, 50frd 5592 . . . . . 6 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
52 frxp3.3 . . . . . . . . 9 (𝜑𝑇 Fr 𝐶)
5352ad3antrrr 728 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 𝑇 Fr 𝐶)
54 imassrn 6024 . . . . . . . . . 10 (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ ran 𝑠
55 rnss 5894 . . . . . . . . . . . 12 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
5655ad2antrl 726 . . . . . . . . . . 11 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
57 rnxpss 6124 . . . . . . . . . . 11 ran ((𝐴 × 𝐵) × 𝐶) ⊆ 𝐶
5856, 57sstrdi 3956 . . . . . . . . . 10 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠𝐶)
5954, 58sstrid 3955 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶)
6059ad2antrr 724 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶)
6111imaex 7853 . . . . . . . . 9 (𝑠 “ {⟨𝑎, 𝑏⟩}) ∈ V
6261a1i 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
6664, 65elimasn 6041 . . . . . . . . . 10 (𝑏 ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
6763, 66sylib 217 . . . . . . . . 9 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
68 imadisj 6032 . . . . . . . . . . 11 ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ (dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅)
69 disjsn 4672 . . . . . . . . . . 11 ((dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
7068, 69bitri 274 . . . . . . . . . 10 ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
7170necon2abii 2994 . . . . . . . . 9 (⟨𝑎, 𝑏⟩ ∈ dom 𝑠 ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
7267, 71sylib 217 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
7353, 60, 62, 72frd 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
7876, 77elimasn 6041 . . . . . . . . . 10 (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
7975, 78sylib 217 . . . . . . . . 9 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
8074, 79eqeltrid 2842 . . . . . . . 8 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ⟨𝑎, 𝑏, 𝑐⟩ ∈ 𝑠)
81 simplrl 775 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
8281ad2antrr 724 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
83 el2xpss 7969 . . . . . . . . . . . 12 ((𝑞𝑠𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → ∃𝑔𝑖 𝑞 = ⟨𝑔, , 𝑖⟩)
8483ancoms 459 . . . . . . . . . . 11 ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑠) → ∃𝑔𝑖 𝑞 = ⟨𝑔, , 𝑖⟩)
8582, 84sylan 580 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ∃𝑔𝑖 𝑞 = ⟨𝑔, , 𝑖⟩)
86 df-ne 2944 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖𝑐 ↔ ¬ 𝑖 = 𝑐)
8786con2bii 357 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑐 ↔ ¬ 𝑖𝑐)
8887biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑐 → ¬ 𝑖𝑐)
8988intnand 489 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑐 → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))
9089adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))
91 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑖 → (𝑓𝑇𝑐𝑖𝑇𝑐))
9291notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑖 → (¬ 𝑓𝑇𝑐 ↔ ¬ 𝑖𝑇𝑐))
93 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
9493adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
95 df-ot 4595 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑎, 𝑏, 𝑖⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑖
96 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠)
9795, 96eqeltrrid 2843 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
98 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑖 ∈ V
9976, 98elimasn 6041 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
10097, 99sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → 𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}))
10192, 94, 100rspcdva 3582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ 𝑖𝑇𝑐)
102 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → 𝑖𝑐)
103102neneqd 2948 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ 𝑖 = 𝑐)
104 ioran 982 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝑖𝑇𝑐𝑖 = 𝑐) ↔ (¬ 𝑖𝑇𝑐 ∧ ¬ 𝑖 = 𝑐))
105101, 103, 104sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ (𝑖𝑇𝑐𝑖 = 𝑐))
106105intn3an3d 1481 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ ((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)))
107106intnanrd 490 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))
10890, 107pm2.61dane 3032 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))
109 oteq2 4840 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = 𝑏 → ⟨𝑎, , 𝑖⟩ = ⟨𝑎, 𝑏, 𝑖⟩)
110109eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . 23 ( = 𝑏 → (⟨𝑎, , 𝑖⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠))
111110anbi2d 629 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠)))
112 neeq1 3006 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( = 𝑏 → (𝑏𝑏𝑏))
113112orbi1d 915 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = 𝑏 → ((𝑏𝑖𝑐) ↔ (𝑏𝑏𝑖𝑐)))
114 neirr 2952 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ¬ 𝑏𝑏
115 orel1 887 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑏𝑏 → ((𝑏𝑏𝑖𝑐) → 𝑖𝑐))
116114, 115ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏𝑏𝑖𝑐) → 𝑖𝑐)
117 olc 866 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖𝑐 → (𝑏𝑏𝑖𝑐))
118116, 117impbii 208 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏𝑏𝑖𝑐) ↔ 𝑖𝑐)
119113, 118bitrdi 286 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = 𝑏 → ((𝑏𝑖𝑐) ↔ 𝑖𝑐))
120119anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . 23 ( = 𝑏 → ((((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)) ↔ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐)))
121120notbid 317 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑏 → (¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)) ↔ ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐)))
122111, 121imbi12d 344 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑏 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))))
123108, 122mpbiri 257 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))))
124123impcom 408 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ = 𝑏) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))
125 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = → (𝑒𝑆𝑏𝑆𝑏))
126125notbid 317 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = → (¬ 𝑒𝑆𝑏 ↔ ¬ 𝑆𝑏))
127 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
128127ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
129 df-ot 4595 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎, , 𝑖⟩ = ⟨⟨𝑎, ⟩, 𝑖
130 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ⟨𝑎, , 𝑖⟩ ∈ 𝑠)
131129, 130eqeltrrid 2843 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠)
132 opex 5421 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎, ⟩ ∈ V
133132, 98opeldm 5863 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑎, ⟩ ∈ dom 𝑠)
134131, 133syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ⟨𝑎, ⟩ ∈ dom 𝑠)
135 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∈ V
13664, 135elimasn 6041 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, ⟩ ∈ dom 𝑠)
137134, 136sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ∈ (dom 𝑠 “ {𝑎}))
138126, 128, 137rspcdva 3582 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ 𝑆𝑏)
139 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → 𝑏)
140139neneqd 2948 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ = 𝑏)
141 ioran 982 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑆𝑏 = 𝑏) ↔ (¬ 𝑆𝑏 ∧ ¬ = 𝑏))
142138, 140, 141sylanbrc 583 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ (𝑆𝑏 = 𝑏))
143142intn3an2d 1480 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ ((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)))
144143intnanrd 490 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))
145124, 144pm2.61dane 3032 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))
146 oteq1 4839 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑎 → ⟨𝑔, , 𝑖⟩ = ⟨𝑎, , 𝑖⟩)
147146eleq1d 2822 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑎 → (⟨𝑔, , 𝑖⟩ ∈ 𝑠 ↔ ⟨𝑎, , 𝑖⟩ ∈ 𝑠))
148147anbi2d 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 (𝑔 = 𝑎 → (𝑖𝑐𝑖𝑐))
152149, 150, 1513orbi123d 1435 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑎 → ((𝑔𝑎𝑏𝑖𝑐) ↔ (𝑎𝑎𝑏𝑖𝑐)))
153 3orass 1090 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑎𝑏𝑖𝑐) ↔ (𝑎𝑎 ∨ (𝑏𝑖𝑐)))
154 neirr 2952 . . . . . . . . . . . . . . . . . . . . . . . . 25 ¬ 𝑎𝑎
155 orel1 887 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑎𝑎 → ((𝑎𝑎 ∨ (𝑏𝑖𝑐)) → (𝑏𝑖𝑐)))
156154, 155ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑎 ∨ (𝑏𝑖𝑐)) → (𝑏𝑖𝑐))
157 olc 866 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏𝑖𝑐) → (𝑎𝑎 ∨ (𝑏𝑖𝑐)))
158156, 157impbii 208 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑎 ∨ (𝑏𝑖𝑐)) ↔ (𝑏𝑖𝑐))
159153, 158bitri 274 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑎𝑏𝑖𝑐) ↔ (𝑏𝑖𝑐))
160152, 159bitrdi 286 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑎 → ((𝑔𝑎𝑏𝑖𝑐) ↔ (𝑏𝑖𝑐)))
161160anbi2d 629 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑎 → ((((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)) ↔ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))))
162161notbid 317 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑎 → (¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)) ↔ ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))))
163148, 162imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑎 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))))
164145, 163mpbiri 257 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))
165164impcom 408 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔 = 𝑎) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))
166 breq1 5108 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑔 → (𝑑𝑅𝑎𝑔𝑅𝑎))
167166notbid 317 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑔 → (¬ 𝑑𝑅𝑎 ↔ ¬ 𝑔𝑅𝑎))
168 simplrr 776 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
169168ad3antrrr 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 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ⟨𝑔, , 𝑖⟩ ∈ 𝑠)
172170, 171eqeltrrid 2843 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠)
173 opex 5421 . . . . . . . . . . . . . . . . . . . . . 22 𝑔, ⟩ ∈ V
174173, 98opeldm 5863 . . . . . . . . . . . . . . . . . . . . 21 (⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑔, ⟩ ∈ dom 𝑠)
175 vex 3449 . . . . . . . . . . . . . . . . . . . . . 22 𝑔 ∈ V
176175, 135opeldm 5863 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑔, ⟩ ∈ dom 𝑠𝑔 ∈ dom dom 𝑠)
177172, 174, 1763syl 18 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → 𝑔 ∈ dom dom 𝑠)
178167, 169, 177rspcdva 3582 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ 𝑔𝑅𝑎)
179 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → 𝑔𝑎)
180179neneqd 2948 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ 𝑔 = 𝑎)
181 ioran 982 . . . . . . . . . . . . . . . . . . 19 (¬ (𝑔𝑅𝑎𝑔 = 𝑎) ↔ (¬ 𝑔𝑅𝑎 ∧ ¬ 𝑔 = 𝑎))
182178, 180, 181sylanbrc 583 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ (𝑔𝑅𝑎𝑔 = 𝑎))
183182intn3an1d 1479 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ ((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)))
184183intnanrd 490 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))
185165, 184pm2.61dane 3032 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))
186185intn3an3d 1481 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))
187 eleq1 2825 . . . . . . . . . . . . . . . 16 (𝑞 = ⟨𝑔, , 𝑖⟩ → (𝑞𝑠 ↔ ⟨𝑔, , 𝑖⟩ ∈ 𝑠))
188187anbi2d 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𝑦))) ∧ 𝑥𝑦))}
191190xpord3lem 8081 . . . . . . . . . . . . . . . . 17 (⟨𝑔, , 𝑖𝑈𝑎, 𝑏, 𝑐⟩ ↔ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))
192189, 191bitrdi 286 . . . . . . . . . . . . . . . 16 (𝑞 = ⟨𝑔, , 𝑖⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))))
193192notbid 317 . . . . . . . . . . . . . . 15 (𝑞 = ⟨𝑔, , 𝑖⟩ → (¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ ¬ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))))
194188, 193imbi12d 344 . . . . . . . . . . . . . 14 (𝑞 = ⟨𝑔, , 𝑖⟩ → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))))
195186, 194mpbiri 257 . . . . . . . . . . . . 13 (𝑞 = ⟨𝑔, , 𝑖⟩ → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
196195com12 32 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → (𝑞 = ⟨𝑔, , 𝑖⟩ → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
197196exlimdv 1936 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → (∃𝑖 𝑞 = ⟨𝑔, , 𝑖⟩ → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
198197exlimdvv 1937 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → (∃𝑔𝑖 𝑞 = ⟨𝑔, , 𝑖⟩ → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
19985, 198mpd 15 . . . . . . . . 9 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩)
200199ralrimiva 3143 . . . . . . . 8 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑞𝑠 ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩)
201 breq2 5109 . . . . . . . . . . 11 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑞𝑈𝑝𝑞𝑈𝑎, 𝑏, 𝑐⟩))
202201notbid 317 . . . . . . . . . 10 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → (¬ 𝑞𝑈𝑝 ↔ ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
203202ralbidv 3174 . . . . . . . . 9 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → (∀𝑞𝑠 ¬ 𝑞𝑈𝑝 ↔ ∀𝑞𝑠 ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
204203rspcev 3581 . . . . . . . 8 ((⟨𝑎, 𝑏, 𝑐⟩ ∈ 𝑠 ∧ ∀𝑞𝑠 ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
20580, 200, 204syl2anc 584 . . . . . . 7 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
20673, 205rexlimddv 3158 . . . . . 6 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
20751, 206rexlimddv 3158 . . . . 5 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
20833, 207rexlimddv 3158 . . . 4 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
209208ex 413 . . 3 (𝜑 → ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝))
210209alrimiv 1930 . 2 (𝜑 → ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝))
211 df-fr 5588 . 2 (𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ↔ ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝))
212210, 211sylibr 233 1 (𝜑𝑈 Fr ((𝐴 × 𝐵) × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3o 1086  w3a 1087  wal 1539   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  cin 3909  wss 3910  c0 4282  {csn 4586  cop 4592  cotp 4594   class class class wbr 5105  {copab 5167   Fr wfr 5585   × cxp 5631  dom cdm 5633  ran crn 5634  cima 5636  Rel wrel 5638  cfv 6496  1st c1st 7919  2nd c2nd 7920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-ot 4595  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-fr 5588  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fv 6504  df-1st 7921  df-2nd 7922
This theorem is referenced by:  xpord3inddlem  8086
  Copyright terms: Public domain W3C validator