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

Theorem frxp3 8132
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 480 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑅 Fr 𝐴)
3 dmss 5893 . . . . . . . . . 10 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
43ad2antrl 725 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
5 dmxpss 6161 . . . . . . . . 9 dom ((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵)
64, 5sstrdi 3987 . . . . . . . 8 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ (𝐴 × 𝐵))
7 dmss 5893 . . . . . . . 8 (dom 𝑠 ⊆ (𝐴 × 𝐵) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
86, 7syl 17 . . . . . . 7 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
9 dmxpss 6161 . . . . . . 7 dom (𝐴 × 𝐵) ⊆ 𝐴
108, 9sstrdi 3987 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠𝐴)
11 vex 3470 . . . . . . . . 9 𝑠 ∈ V
1211dmex 7896 . . . . . . . 8 dom 𝑠 ∈ V
1312dmex 7896 . . . . . . 7 dom dom 𝑠 ∈ V
1413a1i 11 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ∈ V)
15 relxp 5685 . . . . . . . . . . . . 13 Rel ((𝐴 × 𝐵) × 𝐶)
16 relss 5772 . . . . . . . . . . . . 13 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → (Rel ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠))
1715, 16mpi 20 . . . . . . . . . . . 12 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠)
1817adantl 481 . . . . . . . . . . 11 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → Rel 𝑠)
19 reldm0 5918 . . . . . . . . . . 11 (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
2018, 19syl 17 . . . . . . . . . 10 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
21 relxp 5685 . . . . . . . . . . . . . 14 Rel (𝐴 × 𝐵)
22 relss 5772 . . . . . . . . . . . . . 14 (dom ((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel dom ((𝐴 × 𝐵) × 𝐶)))
235, 21, 22mp2 9 . . . . . . . . . . . . 13 Rel dom ((𝐴 × 𝐵) × 𝐶)
24 relss 5772 . . . . . . . . . . . . 13 (dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶) → (Rel dom ((𝐴 × 𝐵) × 𝐶) → Rel dom 𝑠))
253, 23, 24mpisyl 21 . . . . . . . . . . . 12 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → Rel dom 𝑠)
2625adantl 481 . . . . . . . . . . 11 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → Rel dom 𝑠)
27 reldm0 5918 . . . . . . . . . . 11 (Rel dom 𝑠 → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
2826, 27syl 17 . . . . . . . . . 10 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
2920, 28bitrd 279 . . . . . . . . 9 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
3029necon3bid 2977 . . . . . . . 8 ((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅))
3130biimpa 476 . . . . . . 7 (((𝜑𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) ∧ 𝑠 ≠ ∅) → dom dom 𝑠 ≠ ∅)
3231anasss 466 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ≠ ∅)
332, 10, 14, 32frd 5626 . . . . 5 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom dom 𝑠𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
34 frxp3.2 . . . . . . . 8 (𝜑𝑆 Fr 𝐵)
3534ad2antrr 723 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑆 Fr 𝐵)
36 imassrn 6061 . . . . . . . . 9 (dom 𝑠 “ {𝑎}) ⊆ ran dom 𝑠
37 rnss 5929 . . . . . . . . . . 11 (dom 𝑠 ⊆ (𝐴 × 𝐵) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
386, 37syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
39 rnxpss 6162 . . . . . . . . . 10 ran (𝐴 × 𝐵) ⊆ 𝐵
4038, 39sstrdi 3987 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠𝐵)
4136, 40sstrid 3986 . . . . . . . 8 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 “ {𝑎}) ⊆ 𝐵)
4241adantr 480 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ⊆ 𝐵)
4312imaex 7901 . . . . . . . 8 (dom 𝑠 “ {𝑎}) ∈ V
4443a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ∈ V)
45 imadisj 6070 . . . . . . . . . . 11 ((dom 𝑠 “ {𝑎}) = ∅ ↔ (dom dom 𝑠 ∩ {𝑎}) = ∅)
46 disjsn 4708 . . . . . . . . . . 11 ((dom dom 𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠)
4745, 46bitri 275 . . . . . . . . . 10 ((dom 𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠)
4847necon2abii 2983 . . . . . . . . 9 (𝑎 ∈ dom dom 𝑠 ↔ (dom 𝑠 “ {𝑎}) ≠ ∅)
4948biimpi 215 . . . . . . . 8 (𝑎 ∈ dom dom 𝑠 → (dom 𝑠 “ {𝑎}) ≠ ∅)
5049ad2antrl 725 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ≠ ∅)
5135, 42, 44, 50frd 5626 . . . . . 6 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
52 frxp3.3 . . . . . . . . 9 (𝜑𝑇 Fr 𝐶)
5352ad3antrrr 727 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 𝑇 Fr 𝐶)
54 imassrn 6061 . . . . . . . . . 10 (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ ran 𝑠
55 rnss 5929 . . . . . . . . . . . 12 (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
5655ad2antrl 725 . . . . . . . . . . 11 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
57 rnxpss 6162 . . . . . . . . . . 11 ran ((𝐴 × 𝐵) × 𝐶) ⊆ 𝐶
5856, 57sstrdi 3987 . . . . . . . . . 10 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠𝐶)
5954, 58sstrid 3986 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶)
6059ad2antrr 723 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶)
6111imaex 7901 . . . . . . . . 9 (𝑠 “ {⟨𝑎, 𝑏⟩}) ∈ V
6261a1i 11 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ∈ V)
63 simprl 768 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 𝑏 ∈ (dom 𝑠 “ {𝑎}))
64 vex 3470 . . . . . . . . . . 11 𝑎 ∈ V
65 vex 3470 . . . . . . . . . . 11 𝑏 ∈ V
6664, 65elimasn 6079 . . . . . . . . . 10 (𝑏 ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
6763, 66sylib 217 . . . . . . . . 9 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
68 imadisj 6070 . . . . . . . . . . 11 ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ (dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅)
69 disjsn 4708 . . . . . . . . . . 11 ((dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
7068, 69bitri 275 . . . . . . . . . 10 ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
7170necon2abii 2983 . . . . . . . . 9 (⟨𝑎, 𝑏⟩ ∈ dom 𝑠 ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
7267, 71sylib 217 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
7353, 60, 62, 72frd 5626 . . . . . . 7 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
74 df-ot 4630 . . . . . . . . 9 𝑎, 𝑏, 𝑐⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑐
75 simprl 768 . . . . . . . . . 10 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → 𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}))
76 opex 5455 . . . . . . . . . . 11 𝑎, 𝑏⟩ ∈ V
77 vex 3470 . . . . . . . . . . 11 𝑐 ∈ V
7876, 77elimasn 6079 . . . . . . . . . 10 (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
7975, 78sylib 217 . . . . . . . . 9 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
8074, 79eqeltrid 2829 . . . . . . . 8 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ⟨𝑎, 𝑏, 𝑐⟩ ∈ 𝑠)
81 simplrl 774 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
8281ad2antrr 723 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
83 el2xpss 8017 . . . . . . . . . . . 12 ((𝑞𝑠𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → ∃𝑔𝑖 𝑞 = ⟨𝑔, , 𝑖⟩)
8483ancoms 458 . . . . . . . . . . 11 ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑠) → ∃𝑔𝑖 𝑞 = ⟨𝑔, , 𝑖⟩)
8582, 84sylan 579 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ∃𝑔𝑖 𝑞 = ⟨𝑔, , 𝑖⟩)
86 df-ne 2933 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖𝑐 ↔ ¬ 𝑖 = 𝑐)
8786con2bii 357 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑐 ↔ ¬ 𝑖𝑐)
8887biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑐 → ¬ 𝑖𝑐)
8988intnand 488 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑐 → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))
9089adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))
91 breq1 5142 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑖 → (𝑓𝑇𝑐𝑖𝑇𝑐))
9291notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑖 → (¬ 𝑓𝑇𝑐 ↔ ¬ 𝑖𝑇𝑐))
93 simplrr 775 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
9493adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
95 df-ot 4630 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑎, 𝑏, 𝑖⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑖
96 simplr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠)
9795, 96eqeltrrid 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
98 vex 3470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑖 ∈ V
9976, 98elimasn 6079 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
10097, 99sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → 𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}))
10192, 94, 100rspcdva 3605 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ 𝑖𝑇𝑐)
102 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → 𝑖𝑐)
103102neneqd 2937 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ 𝑖 = 𝑐)
104 ioran 980 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝑖𝑇𝑐𝑖 = 𝑐) ↔ (¬ 𝑖𝑇𝑐 ∧ ¬ 𝑖 = 𝑐))
105101, 103, 104sylanbrc 582 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ (𝑖𝑇𝑐𝑖 = 𝑐))
106105intn3an3d 1477 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ ((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)))
107106intnanrd 489 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖𝑐) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))
10890, 107pm2.61dane 3021 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))
109 oteq2 4876 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = 𝑏 → ⟨𝑎, , 𝑖⟩ = ⟨𝑎, 𝑏, 𝑖⟩)
110109eleq1d 2810 . . . . . . . . . . . . . . . . . . . . . . 23 ( = 𝑏 → (⟨𝑎, , 𝑖⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠))
111110anbi2d 628 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠)))
112 neeq1 2995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( = 𝑏 → (𝑏𝑏𝑏))
113112orbi1d 913 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = 𝑏 → ((𝑏𝑖𝑐) ↔ (𝑏𝑏𝑖𝑐)))
114 neirr 2941 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ¬ 𝑏𝑏
115 orel1 885 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑏𝑏 → ((𝑏𝑏𝑖𝑐) → 𝑖𝑐))
116114, 115ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏𝑏𝑖𝑐) → 𝑖𝑐)
117 olc 865 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖𝑐 → (𝑏𝑏𝑖𝑐))
118116, 117impbii 208 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏𝑏𝑖𝑐) ↔ 𝑖𝑐)
119113, 118bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = 𝑏 → ((𝑏𝑖𝑐) ↔ 𝑖𝑐))
120119anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . 23 ( = 𝑏 → ((((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)) ↔ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐)))
121120notbid 318 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑏 → (¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)) ↔ ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐)))
122111, 121imbi12d 344 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑏 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ 𝑖𝑐))))
123108, 122mpbiri 258 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))))
124123impcom 407 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ = 𝑏) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))
125 breq1 5142 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = → (𝑒𝑆𝑏𝑆𝑏))
126125notbid 318 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = → (¬ 𝑒𝑆𝑏 ↔ ¬ 𝑆𝑏))
127 simplrr 775 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
128127ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
129 df-ot 4630 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎, , 𝑖⟩ = ⟨⟨𝑎, ⟩, 𝑖
130 simplr 766 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ⟨𝑎, , 𝑖⟩ ∈ 𝑠)
131129, 130eqeltrrid 2830 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠)
132 opex 5455 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎, ⟩ ∈ V
133132, 98opeldm 5898 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨⟨𝑎, ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑎, ⟩ ∈ dom 𝑠)
134131, 133syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ⟨𝑎, ⟩ ∈ dom 𝑠)
135 vex 3470 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∈ V
13664, 135elimasn 6079 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, ⟩ ∈ dom 𝑠)
137134, 136sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ∈ (dom 𝑠 “ {𝑎}))
138126, 128, 137rspcdva 3605 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ 𝑆𝑏)
139 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → 𝑏)
140139neneqd 2937 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ = 𝑏)
141 ioran 980 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑆𝑏 = 𝑏) ↔ (¬ 𝑆𝑏 ∧ ¬ = 𝑏))
142138, 140, 141sylanbrc 582 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ (𝑆𝑏 = 𝑏))
143142intn3an2d 1476 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ ((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)))
144143intnanrd 489 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) ∧ 𝑏) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))
145124, 144pm2.61dane 3021 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))
146 oteq1 4875 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑎 → ⟨𝑔, , 𝑖⟩ = ⟨𝑎, , 𝑖⟩)
147146eleq1d 2810 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑎 → (⟨𝑔, , 𝑖⟩ ∈ 𝑠 ↔ ⟨𝑎, , 𝑖⟩ ∈ 𝑠))
148147anbi2d 628 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠)))
149 neeq1 2995 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝑎 → (𝑔𝑎𝑎𝑎))
150 biidd 262 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝑎 → (𝑏𝑏))
151 biidd 262 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝑎 → (𝑖𝑐𝑖𝑐))
152149, 150, 1513orbi123d 1431 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑎 → ((𝑔𝑎𝑏𝑖𝑐) ↔ (𝑎𝑎𝑏𝑖𝑐)))
153 3orass 1087 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑎𝑏𝑖𝑐) ↔ (𝑎𝑎 ∨ (𝑏𝑖𝑐)))
154 neirr 2941 . . . . . . . . . . . . . . . . . . . . . . . . 25 ¬ 𝑎𝑎
155 orel1 885 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑎𝑎 → ((𝑎𝑎 ∨ (𝑏𝑖𝑐)) → (𝑏𝑖𝑐)))
156154, 155ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑎 ∨ (𝑏𝑖𝑐)) → (𝑏𝑖𝑐))
157 olc 865 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏𝑖𝑐) → (𝑎𝑎 ∨ (𝑏𝑖𝑐)))
158156, 157impbii 208 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑎 ∨ (𝑏𝑖𝑐)) ↔ (𝑏𝑖𝑐))
159153, 158bitri 275 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑎𝑏𝑖𝑐) ↔ (𝑏𝑖𝑐))
160152, 159bitrdi 287 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑎 → ((𝑔𝑎𝑏𝑖𝑐) ↔ (𝑏𝑖𝑐)))
161160anbi2d 628 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑎 → ((((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)) ↔ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))))
162161notbid 318 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑎 → (¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)) ↔ ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐))))
163148, 162imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑎 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑏𝑖𝑐)))))
164145, 163mpbiri 258 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))
165164impcom 407 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔 = 𝑎) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))
166 breq1 5142 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑔 → (𝑑𝑅𝑎𝑔𝑅𝑎))
167166notbid 318 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑔 → (¬ 𝑑𝑅𝑎 ↔ ¬ 𝑔𝑅𝑎))
168 simplrr 775 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
169168ad3antrrr 727 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
170 df-ot 4630 . . . . . . . . . . . . . . . . . . . . . 22 𝑔, , 𝑖⟩ = ⟨⟨𝑔, ⟩, 𝑖
171 simplr 766 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ⟨𝑔, , 𝑖⟩ ∈ 𝑠)
172170, 171eqeltrrid 2830 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠)
173 opex 5455 . . . . . . . . . . . . . . . . . . . . . 22 𝑔, ⟩ ∈ V
174173, 98opeldm 5898 . . . . . . . . . . . . . . . . . . . . 21 (⟨⟨𝑔, ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑔, ⟩ ∈ dom 𝑠)
175 vex 3470 . . . . . . . . . . . . . . . . . . . . . 22 𝑔 ∈ V
176175, 135opeldm 5898 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑔, ⟩ ∈ dom 𝑠𝑔 ∈ dom dom 𝑠)
177172, 174, 1763syl 18 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → 𝑔 ∈ dom dom 𝑠)
178167, 169, 177rspcdva 3605 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ 𝑔𝑅𝑎)
179 simpr 484 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → 𝑔𝑎)
180179neneqd 2937 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ 𝑔 = 𝑎)
181 ioran 980 . . . . . . . . . . . . . . . . . . 19 (¬ (𝑔𝑅𝑎𝑔 = 𝑎) ↔ (¬ 𝑔𝑅𝑎 ∧ ¬ 𝑔 = 𝑎))
182178, 180, 181sylanbrc 582 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ (𝑔𝑅𝑎𝑔 = 𝑎))
183182intn3an1d 1475 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ ((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)))
184183intnanrd 489 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) ∧ 𝑔𝑎) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))
185165, 184pm2.61dane 3021 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))
186185intn3an3d 1477 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))
187 eleq1 2813 . . . . . . . . . . . . . . . 16 (𝑞 = ⟨𝑔, , 𝑖⟩ → (𝑞𝑠 ↔ ⟨𝑔, , 𝑖⟩ ∈ 𝑠))
188187anbi2d 628 . . . . . . . . . . . . . . 15 (𝑞 = ⟨𝑔, , 𝑖⟩ → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠)))
189 breq1 5142 . . . . . . . . . . . . . . . . 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 8130 . . . . . . . . . . . . . . . . 17 (⟨𝑔, , 𝑖𝑈𝑎, 𝑏, 𝑐⟩ ↔ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))
192189, 191bitrdi 287 . . . . . . . . . . . . . . . 16 (𝑞 = ⟨𝑔, , 𝑖⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))))
193192notbid 318 . . . . . . . . . . . . . . 15 (𝑞 = ⟨𝑔, , 𝑖⟩ → (¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ ¬ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐)))))
194188, 193imbi12d 344 . . . . . . . . . . . . . 14 (𝑞 = ⟨𝑔, , 𝑖⟩ → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, , 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑔𝑅𝑎𝑔 = 𝑎) ∧ (𝑆𝑏 = 𝑏) ∧ (𝑖𝑇𝑐𝑖 = 𝑐)) ∧ (𝑔𝑎𝑏𝑖𝑐))))))
195186, 194mpbiri 258 . . . . . . . . . . . . 13 (𝑞 = ⟨𝑔, , 𝑖⟩ → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
196195com12 32 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → (𝑞 = ⟨𝑔, , 𝑖⟩ → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
197196exlimdv 1928 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → (∃𝑖 𝑞 = ⟨𝑔, , 𝑖⟩ → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
198197exlimdvv 1929 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → (∃𝑔𝑖 𝑞 = ⟨𝑔, , 𝑖⟩ → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
19985, 198mpd 15 . . . . . . . . 9 ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩)
200199ralrimiva 3138 . . . . . . . 8 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑞𝑠 ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩)
201 breq2 5143 . . . . . . . . . . 11 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑞𝑈𝑝𝑞𝑈𝑎, 𝑏, 𝑐⟩))
202201notbid 318 . . . . . . . . . 10 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → (¬ 𝑞𝑈𝑝 ↔ ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
203202ralbidv 3169 . . . . . . . . 9 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → (∀𝑞𝑠 ¬ 𝑞𝑈𝑝 ↔ ∀𝑞𝑠 ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
204203rspcev 3604 . . . . . . . 8 ((⟨𝑎, 𝑏, 𝑐⟩ ∈ 𝑠 ∧ ∀𝑞𝑠 ¬ 𝑞𝑈𝑎, 𝑏, 𝑐⟩) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
20580, 200, 204syl2anc 583 . . . . . . 7 (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
20673, 205rexlimddv 3153 . . . . . 6 ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
20751, 206rexlimddv 3153 . . . . 5 (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
20833, 207rexlimddv 3153 . . . 4 ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝)
209208ex 412 . . 3 (𝜑 → ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝))
210209alrimiv 1922 . 2 (𝜑 → ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝))
211 df-fr 5622 . 2 (𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ↔ ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑈𝑝))
212210, 211sylibr 233 1 (𝜑𝑈 Fr ((𝐴 × 𝐵) × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 844  w3o 1083  w3a 1084  wal 1531   = wceq 1533  wex 1773  wcel 2098  wne 2932  wral 3053  wrex 3062  Vcvv 3466  cin 3940  wss 3941  c0 4315  {csn 4621  cop 4627  cotp 4629   class class class wbr 5139  {copab 5201   Fr wfr 5619   × cxp 5665  dom cdm 5667  ran crn 5668  cima 5670  Rel wrel 5672  cfv 6534  1st c1st 7967  2nd c2nd 7968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418  ax-un 7719
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-ot 4630  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-fr 5622  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fv 6542  df-1st 7969  df-2nd 7970
This theorem is referenced by:  xpord3inddlem  8135
  Copyright terms: Public domain W3C validator