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

Theorem frxp2 8081
Description: Another way of giving a well-founded order to a Cartesian product of two classes. (Contributed by Scott Fenton, 19-Aug-2024.)
Hypotheses
Ref Expression
xpord2.1 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st𝑥)𝑅(1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥)𝑆(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))}
frxp2.1 (𝜑𝑅 Fr 𝐴)
frxp2.2 (𝜑𝑆 Fr 𝐵)
Assertion
Ref Expression
frxp2 (𝜑𝑇 Fr (𝐴 × 𝐵))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑇(𝑥,𝑦)

Proof of Theorem frxp2
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑝 𝑞 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmss 5863 . . . . . . . 8 (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
21ad2antrl 727 . . . . . . 7 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
3 dmxpss 6128 . . . . . . 7 dom (𝐴 × 𝐵) ⊆ 𝐴
42, 3sstrdi 3961 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠𝐴)
5 simprr 772 . . . . . . 7 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑠 ≠ ∅)
6 relxp 5656 . . . . . . . . . . 11 Rel (𝐴 × 𝐵)
7 relss 5742 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
86, 7mpi 20 . . . . . . . . . 10 (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
98ad2antrl 727 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → Rel 𝑠)
10 reldm0 5888 . . . . . . . . 9 (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
119, 10syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1211necon3bid 2989 . . . . . . 7 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
135, 12mpbid 231 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ≠ ∅)
14 frxp2.1 . . . . . . . . 9 (𝜑𝑅 Fr 𝐴)
1514adantr 482 . . . . . . . 8 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑅 Fr 𝐴)
16 df-fr 5593 . . . . . . . 8 (𝑅 Fr 𝐴 ↔ ∀𝑐((𝑐𝐴𝑐 ≠ ∅) → ∃𝑎𝑐𝑏𝑐 ¬ 𝑏𝑅𝑎))
1715, 16sylib 217 . . . . . . 7 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∀𝑐((𝑐𝐴𝑐 ≠ ∅) → ∃𝑎𝑐𝑏𝑐 ¬ 𝑏𝑅𝑎))
18 vex 3452 . . . . . . . . 9 𝑠 ∈ V
1918dmex 7853 . . . . . . . 8 dom 𝑠 ∈ V
20 sseq1 3974 . . . . . . . . . 10 (𝑐 = dom 𝑠 → (𝑐𝐴 ↔ dom 𝑠𝐴))
21 neeq1 3007 . . . . . . . . . 10 (𝑐 = dom 𝑠 → (𝑐 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
2220, 21anbi12d 632 . . . . . . . . 9 (𝑐 = dom 𝑠 → ((𝑐𝐴𝑐 ≠ ∅) ↔ (dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅)))
23 raleq 3312 . . . . . . . . . 10 (𝑐 = dom 𝑠 → (∀𝑏𝑐 ¬ 𝑏𝑅𝑎 ↔ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
2423rexeqbi1dv 3311 . . . . . . . . 9 (𝑐 = dom 𝑠 → (∃𝑎𝑐𝑏𝑐 ¬ 𝑏𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
2522, 24imbi12d 345 . . . . . . . 8 (𝑐 = dom 𝑠 → (((𝑐𝐴𝑐 ≠ ∅) → ∃𝑎𝑐𝑏𝑐 ¬ 𝑏𝑅𝑎) ↔ ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)))
2619, 25spcv 3567 . . . . . . 7 (∀𝑐((𝑐𝐴𝑐 ≠ ∅) → ∃𝑎𝑐𝑏𝑐 ¬ 𝑏𝑅𝑎) → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
2717, 26syl 17 . . . . . 6 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
284, 13, 27mp2and 698 . . . . 5 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom 𝑠𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
29 imassrn 6029 . . . . . . . 8 (𝑠 “ {𝑎}) ⊆ ran 𝑠
30 rnss 5899 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
3130ad2antrl 727 . . . . . . . . . 10 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
3231adantr 482 . . . . . . . . 9 (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
33 rnxpss 6129 . . . . . . . . 9 ran (𝐴 × 𝐵) ⊆ 𝐵
3432, 33sstrdi 3961 . . . . . . . 8 (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠𝐵)
3529, 34sstrid 3960 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ⊆ 𝐵)
36 simprl 770 . . . . . . . 8 (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → 𝑎 ∈ dom 𝑠)
37 imadisj 6037 . . . . . . . . . 10 ((𝑠 “ {𝑎}) = ∅ ↔ (dom 𝑠 ∩ {𝑎}) = ∅)
38 disjsn 4677 . . . . . . . . . 10 ((dom 𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
3937, 38bitri 275 . . . . . . . . 9 ((𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
4039necon2abii 2995 . . . . . . . 8 (𝑎 ∈ dom 𝑠 ↔ (𝑠 “ {𝑎}) ≠ ∅)
4136, 40sylib 217 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ≠ ∅)
42 frxp2.2 . . . . . . . . . 10 (𝜑𝑆 Fr 𝐵)
43 df-fr 5593 . . . . . . . . . 10 (𝑆 Fr 𝐵 ↔ ∀𝑒((𝑒𝐵𝑒 ≠ ∅) → ∃𝑐𝑒𝑑𝑒 ¬ 𝑑𝑆𝑐))
4442, 43sylib 217 . . . . . . . . 9 (𝜑 → ∀𝑒((𝑒𝐵𝑒 ≠ ∅) → ∃𝑐𝑒𝑑𝑒 ¬ 𝑑𝑆𝑐))
4544ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∀𝑒((𝑒𝐵𝑒 ≠ ∅) → ∃𝑐𝑒𝑑𝑒 ¬ 𝑑𝑆𝑐))
4618imaex 7858 . . . . . . . . 9 (𝑠 “ {𝑎}) ∈ V
47 sseq1 3974 . . . . . . . . . . 11 (𝑒 = (𝑠 “ {𝑎}) → (𝑒𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
48 neeq1 3007 . . . . . . . . . . 11 (𝑒 = (𝑠 “ {𝑎}) → (𝑒 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
4947, 48anbi12d 632 . . . . . . . . . 10 (𝑒 = (𝑠 “ {𝑎}) → ((𝑒𝐵𝑒 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
50 raleq 3312 . . . . . . . . . . 11 (𝑒 = (𝑠 “ {𝑎}) → (∀𝑑𝑒 ¬ 𝑑𝑆𝑐 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
5150rexeqbi1dv 3311 . . . . . . . . . 10 (𝑒 = (𝑠 “ {𝑎}) → (∃𝑐𝑒𝑑𝑒 ¬ 𝑑𝑆𝑐 ↔ ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
5249, 51imbi12d 345 . . . . . . . . 9 (𝑒 = (𝑠 “ {𝑎}) → (((𝑒𝐵𝑒 ≠ ∅) → ∃𝑐𝑒𝑑𝑒 ¬ 𝑑𝑆𝑐) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)))
5346, 52spcv 3567 . . . . . . . 8 (∀𝑒((𝑒𝐵𝑒 ≠ ∅) → ∃𝑐𝑒𝑑𝑒 ¬ 𝑑𝑆𝑐) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
5445, 53syl 17 . . . . . . 7 (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
5535, 41, 54mp2and 698 . . . . . 6 (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
56 simprl 770 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → 𝑐 ∈ (𝑠 “ {𝑎}))
57 vex 3452 . . . . . . . . 9 𝑎 ∈ V
58 vex 3452 . . . . . . . . 9 𝑐 ∈ V
5957, 58elimasn 6046 . . . . . . . 8 (𝑐 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑐⟩ ∈ 𝑠)
6056, 59sylib 217 . . . . . . 7 ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ⟨𝑎, 𝑐⟩ ∈ 𝑠)
619ad2antrr 725 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → Rel 𝑠)
62 elrel 5759 . . . . . . . . . 10 ((Rel 𝑠𝑞𝑠) → ∃𝑒𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
6361, 62sylan 581 . . . . . . . . 9 (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞𝑠) → ∃𝑒𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
64 breq1 5113 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑓 → (𝑑𝑆𝑐𝑓𝑆𝑐))
6564notbid 318 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑓 → (¬ 𝑑𝑆𝑐 ↔ ¬ 𝑓𝑆𝑐))
66 simplrr 777 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
67 vex 3452 . . . . . . . . . . . . . . . . . . . . 21 𝑓 ∈ V
6857, 67elimasn 6046 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠)
6968biimpri 227 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑓⟩ ∈ 𝑠𝑓 ∈ (𝑠 “ {𝑎}))
7069adantl 483 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → 𝑓 ∈ (𝑠 “ {𝑎}))
7165, 66, 70rspcdva 3585 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ 𝑓𝑆𝑐)
7271intnanrd 491 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐𝑓𝑐))
73 opeq1 4835 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑎 → ⟨𝑒, 𝑓⟩ = ⟨𝑎, 𝑓⟩)
7473eleq1d 2823 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑎 → (⟨𝑒, 𝑓⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠))
7574anbi2d 630 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠)))
76 3anass 1096 . . . . . . . . . . . . . . . . . . 19 (((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)) ↔ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐))))
77 olc 867 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑎 → (𝑒𝑅𝑎𝑒 = 𝑎))
7877biantrurd 534 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑎 → (((𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)) ↔ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)))))
79 neeq1 3007 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = 𝑎 → (𝑒𝑎𝑎𝑎))
8079orbi1d 916 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = 𝑎 → ((𝑒𝑎𝑓𝑐) ↔ (𝑎𝑎𝑓𝑐)))
81 neirr 2953 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ 𝑎𝑎
82 biorf 936 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑎𝑎 → (𝑓𝑐 ↔ (𝑎𝑎𝑓𝑐)))
8381, 82ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓𝑐 ↔ (𝑎𝑎𝑓𝑐))
8480, 83bitr4di 289 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = 𝑎 → ((𝑒𝑎𝑓𝑐) ↔ 𝑓𝑐))
8584anbi2d 630 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑎 → (((𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)) ↔ ((𝑓𝑆𝑐𝑓 = 𝑐) ∧ 𝑓𝑐)))
86 andir 1008 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓𝑆𝑐𝑓 = 𝑐) ∧ 𝑓𝑐) ↔ ((𝑓𝑆𝑐𝑓𝑐) ∨ (𝑓 = 𝑐𝑓𝑐)))
87 nonconne 2956 . . . . . . . . . . . . . . . . . . . . . . 23 ¬ (𝑓 = 𝑐𝑓𝑐)
8887biorfi 938 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑆𝑐𝑓𝑐) ↔ ((𝑓𝑆𝑐𝑓𝑐) ∨ (𝑓 = 𝑐𝑓𝑐)))
8986, 88bitr4i 278 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓𝑆𝑐𝑓 = 𝑐) ∧ 𝑓𝑐) ↔ (𝑓𝑆𝑐𝑓𝑐))
9085, 89bitrdi 287 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑎 → (((𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)) ↔ (𝑓𝑆𝑐𝑓𝑐)))
9178, 90bitr3d 281 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑎 → (((𝑒𝑅𝑎𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐))) ↔ (𝑓𝑆𝑐𝑓𝑐)))
9276, 91bitrid 283 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑎 → (((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)) ↔ (𝑓𝑆𝑐𝑓𝑐)))
9392notbid 318 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑎 → (¬ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)) ↔ ¬ (𝑓𝑆𝑐𝑓𝑐)))
9475, 93imbi12d 345 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐))) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐𝑓𝑐))))
9572, 94mpbiri 258 . . . . . . . . . . . . . . 15 (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐))))
9695impcom 409 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 = 𝑎) → ¬ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)))
97 breq1 5113 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑒 → (𝑏𝑅𝑎𝑒𝑅𝑎))
9897notbid 318 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑒 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑒𝑅𝑎))
99 simplrr 777 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
10099ad2antrr 725 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒𝑎) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
101 vex 3452 . . . . . . . . . . . . . . . . . . . 20 𝑒 ∈ V
102101, 67opeldm 5868 . . . . . . . . . . . . . . . . . . 19 (⟨𝑒, 𝑓⟩ ∈ 𝑠𝑒 ∈ dom 𝑠)
103102adantl 483 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → 𝑒 ∈ dom 𝑠)
104103adantr 482 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒𝑎) → 𝑒 ∈ dom 𝑠)
10598, 100, 104rspcdva 3585 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒𝑎) → ¬ 𝑒𝑅𝑎)
106 simpr 486 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒𝑎) → 𝑒𝑎)
107106neneqd 2949 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒𝑎) → ¬ 𝑒 = 𝑎)
108 ioran 983 . . . . . . . . . . . . . . . 16 (¬ (𝑒𝑅𝑎𝑒 = 𝑎) ↔ (¬ 𝑒𝑅𝑎 ∧ ¬ 𝑒 = 𝑎))
109105, 107, 108sylanbrc 584 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒𝑎) → ¬ (𝑒𝑅𝑎𝑒 = 𝑎))
110109intn3an1d 1480 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒𝑎) → ¬ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)))
11196, 110pm2.61dane 3033 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)))
112111intn3an3d 1482 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝐴𝑓𝐵) ∧ (𝑎𝐴𝑐𝐵) ∧ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐))))
113 eleq1 2826 . . . . . . . . . . . . . 14 (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑠 ↔ ⟨𝑒, 𝑓⟩ ∈ 𝑠))
114113anbi2d 630 . . . . . . . . . . . . 13 (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠)))
115 breq1 5113 . . . . . . . . . . . . . . 15 (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇𝑎, 𝑐⟩ ↔ ⟨𝑒, 𝑓𝑇𝑎, 𝑐⟩))
116 xpord2.1 . . . . . . . . . . . . . . . 16 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st𝑥)𝑅(1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥)𝑆(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))}
117116xpord2lem 8079 . . . . . . . . . . . . . . 15 (⟨𝑒, 𝑓𝑇𝑎, 𝑐⟩ ↔ ((𝑒𝐴𝑓𝐵) ∧ (𝑎𝐴𝑐𝐵) ∧ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐))))
118115, 117bitrdi 287 . . . . . . . . . . . . . 14 (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇𝑎, 𝑐⟩ ↔ ((𝑒𝐴𝑓𝐵) ∧ (𝑎𝐴𝑐𝐵) ∧ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)))))
119118notbid 318 . . . . . . . . . . . . 13 (𝑞 = ⟨𝑒, 𝑓⟩ → (¬ 𝑞𝑇𝑎, 𝑐⟩ ↔ ¬ ((𝑒𝐴𝑓𝐵) ∧ (𝑎𝐴𝑐𝐵) ∧ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐)))))
120114, 119imbi12d 345 . . . . . . . . . . . 12 (𝑞 = ⟨𝑒, 𝑓⟩ → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑇𝑎, 𝑐⟩) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝐴𝑓𝐵) ∧ (𝑎𝐴𝑐𝐵) ∧ ((𝑒𝑅𝑎𝑒 = 𝑎) ∧ (𝑓𝑆𝑐𝑓 = 𝑐) ∧ (𝑒𝑎𝑓𝑐))))))
121112, 120mpbiri 258 . . . . . . . . . . 11 (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑇𝑎, 𝑐⟩))
122121com12 32 . . . . . . . . . 10 (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞𝑠) → (𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇𝑎, 𝑐⟩))
123122exlimdvv 1938 . . . . . . . . 9 (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞𝑠) → (∃𝑒𝑓 𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇𝑎, 𝑐⟩))
12463, 123mpd 15 . . . . . . . 8 (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞𝑠) → ¬ 𝑞𝑇𝑎, 𝑐⟩)
125124ralrimiva 3144 . . . . . . 7 ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑞𝑠 ¬ 𝑞𝑇𝑎, 𝑐⟩)
126 breq2 5114 . . . . . . . . . 10 (𝑝 = ⟨𝑎, 𝑐⟩ → (𝑞𝑇𝑝𝑞𝑇𝑎, 𝑐⟩))
127126notbid 318 . . . . . . . . 9 (𝑝 = ⟨𝑎, 𝑐⟩ → (¬ 𝑞𝑇𝑝 ↔ ¬ 𝑞𝑇𝑎, 𝑐⟩))
128127ralbidv 3175 . . . . . . . 8 (𝑝 = ⟨𝑎, 𝑐⟩ → (∀𝑞𝑠 ¬ 𝑞𝑇𝑝 ↔ ∀𝑞𝑠 ¬ 𝑞𝑇𝑎, 𝑐⟩))
129128rspcev 3584 . . . . . . 7 ((⟨𝑎, 𝑐⟩ ∈ 𝑠 ∧ ∀𝑞𝑠 ¬ 𝑞𝑇𝑎, 𝑐⟩) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑇𝑝)
13060, 125, 129syl2anc 585 . . . . . 6 ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑇𝑝)
13155, 130rexlimddv 3159 . . . . 5 (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑇𝑝)
13228, 131rexlimddv 3159 . . . 4 ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑇𝑝)
133132ex 414 . . 3 (𝜑 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑇𝑝))
134133alrimiv 1931 . 2 (𝜑 → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑇𝑝))
135 df-fr 5593 . 2 (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝𝑠𝑞𝑠 ¬ 𝑞𝑇𝑝))
136134, 135sylibr 233 1 (𝜑𝑇 Fr (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3a 1088  wal 1540   = wceq 1542  wex 1782  wcel 2107  wne 2944  wral 3065  wrex 3074  cin 3914  wss 3915  c0 4287  {csn 4591  cop 4597   class class class wbr 5110  {copab 5172   Fr wfr 5590   × cxp 5636  dom cdm 5638  ran crn 5639  cima 5641  Rel wrel 5643  cfv 6501  1st c1st 7924  2nd c2nd 7925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-fr 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fv 6509  df-1st 7926  df-2nd 7927
This theorem is referenced by:  xpord2indlem  8084  on2recsfn  8618  on2recsov  8619  noxpordfr  27285
  Copyright terms: Public domain W3C validator