frxp2 - Metamath Proof Explorer

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

Theorem frxp2 8135

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	⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
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.

Step	Hyp	Ref	Expression
1		dmss 5902	. . . . . . . 8 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
2	1	ad2antrl 725	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
3		dmxpss 6170	. . . . . . 7 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
4	2, 3	sstrdi 3994	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ 𝐴)
5		simprr 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑠 ≠ ∅)
6		relxp 5694	. . . . . . . . . . 11 ⊢ Rel (𝐴 × 𝐵)
7		relss 5781	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
8	6, 7	mpi 20	. . . . . . . . . 10 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
9	8	ad2antrl 725	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → Rel 𝑠)
10		reldm0 5927	. . . . . . . . 9 ⊢ (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
11	9, 10	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
12	11	necon3bid 2984	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
13	5, 12	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ≠ ∅)
14		frxp2.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 Fr 𝐴)
15	14	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑅 Fr 𝐴)
16		df-fr 5631	. . . . . . . 8 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎))
17	15, 16	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎))
18		vex 3477	. . . . . . . . 9 ⊢ 𝑠 ∈ V
19	18	dmex 7906	. . . . . . . 8 ⊢ dom 𝑠 ∈ V
20		sseq1 4007	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (𝑐 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴))
21		neeq1 3002	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (𝑐 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
22	20, 21	anbi12d 630	. . . . . . . . 9 ⊢ (𝑐 = dom 𝑠 → ((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) ↔ (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅)))
23		raleq 3321	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎 ↔ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
24	23	rexeqbi1dv 3333	. . . . . . . . 9 ⊢ (𝑐 = dom 𝑠 → (∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
25	22, 24	imbi12d 344	. . . . . . . 8 ⊢ (𝑐 = dom 𝑠 → (((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎) ↔ ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)))
26	19, 25	spcv 3595	. . . . . . 7 ⊢ (∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
27	17, 26	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
28	4, 13, 27	mp2and 696	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
29		imassrn 6070	. . . . . . . 8 ⊢ (𝑠 “ {𝑎}) ⊆ ran 𝑠
30		rnss 5938	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
31	30	ad2antrl 725	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
32	31	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
33		rnxpss 6171	. . . . . . . . 9 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
34	32, 33	sstrdi 3994	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠 ⊆ 𝐵)
35	29, 34	sstrid 3993	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ⊆ 𝐵)
36		simprl 768	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → 𝑎 ∈ dom 𝑠)
37		imadisj 6079	. . . . . . . . . 10 ⊢ ((𝑠 “ {𝑎}) = ∅ ↔ (dom 𝑠 ∩ {𝑎}) = ∅)
38		disjsn 4715	. . . . . . . . . 10 ⊢ ((dom 𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
39	37, 38	bitri 275	. . . . . . . . 9 ⊢ ((𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
40	39	necon2abii 2990	. . . . . . . 8 ⊢ (𝑎 ∈ dom 𝑠 ↔ (𝑠 “ {𝑎}) ≠ ∅)
41	36, 40	sylib 217	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ≠ ∅)
42		frxp2.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 Fr 𝐵)
43		df-fr 5631	. . . . . . . . . 10 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
44	42, 43	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
45	44	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
46	18	imaex 7911	. . . . . . . . 9 ⊢ (𝑠 “ {𝑎}) ∈ V
47		sseq1 4007	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (𝑒 ⊆ 𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
48		neeq1 3002	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (𝑒 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
49	47, 48	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑒 = (𝑠 “ {𝑎}) → ((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
50		raleq 3321	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
51	50	rexeqbi1dv 3333	. . . . . . . . . 10 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐 ↔ ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
52	49, 51	imbi12d 344	. . . . . . . . 9 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)))
53	46, 52	spcv 3595	. . . . . . . 8 ⊢ (∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
54	45, 53	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
55	35, 41, 54	mp2and 696	. . . . . 6 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
56		simprl 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → 𝑐 ∈ (𝑠 “ {𝑎}))
57		vex 3477	. . . . . . . . 9 ⊢ 𝑎 ∈ V
58		vex 3477	. . . . . . . . 9 ⊢ 𝑐 ∈ V
59	57, 58	elimasn 6088	. . . . . . . 8 ⊢ (𝑐 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑐⟩ ∈ 𝑠)
60	56, 59	sylib 217	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ⟨𝑎, 𝑐⟩ ∈ 𝑠)
61	9	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → Rel 𝑠)
62		elrel 5798	. . . . . . . . . 10 ⊢ ((Rel 𝑠 ∧ 𝑞 ∈ 𝑠) → ∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
63	61, 62	sylan 579	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
64		breq1 5151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑓 → (𝑑𝑆𝑐 ↔ 𝑓𝑆𝑐))
65	64	notbid 318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑓 → (¬ 𝑑𝑆𝑐 ↔ ¬ 𝑓𝑆𝑐))
66		simplrr 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
67		vex 3477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑓 ∈ V
68	57, 67	elimasn 6088	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠)
69	68	biimpri 227	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑎, 𝑓⟩ ∈ 𝑠 → 𝑓 ∈ (𝑠 “ {𝑎}))
70	69	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → 𝑓 ∈ (𝑠 “ {𝑎}))
71	65, 66, 70	rspcdva 3613	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ 𝑓𝑆𝑐)
72	71	intnanrd 489	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))
73		opeq1 4873	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑎 → ⟨𝑒, 𝑓⟩ = ⟨𝑎, 𝑓⟩)
74	73	eleq1d 2817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑎 → (⟨𝑒, 𝑓⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠))
75	74	anbi2d 628	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠)))
76		3anass 1094	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
77		olc 865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑎 → (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎))
78	77	biantrurd 532	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
79		neeq1 3002	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = 𝑎 → (𝑒 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
80	79	orbi1d 914	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑒 = 𝑎 → ((𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
81		neirr 2948	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ 𝑎 ≠ 𝑎
82		biorf 934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑎 ≠ 𝑎 → (𝑓 ≠ 𝑐 ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
83	81, 82	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ≠ 𝑐 ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))
84	80, 83	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = 𝑎 → ((𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐) ↔ 𝑓 ≠ 𝑐))
85	84	anbi2d 628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐)))
86		andir 1006	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐) ↔ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ∨ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)))
87		nonconne 2951	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ¬ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)
88	87	biorfi 936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ↔ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ∨ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)))
89	86, 88	bitr4i 278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))
90	85, 89	bitrdi 287	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
91	78, 90	bitr3d 281	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑎 → (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
92	76, 91	bitrid 283	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑎 → (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
93	92	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑎 → (¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
94	75, 93	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))))
95	72, 94	mpbiri 258	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
96	95	impcom 407	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 = 𝑎) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
97		breq1 5151	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑒 → (𝑏𝑅𝑎 ↔ 𝑒𝑅𝑎))
98	97	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑒 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑒𝑅𝑎))
99		simplrr 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
100	99	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
101		vex 3477	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑒 ∈ V
102	101, 67	opeldm 5907	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑒, 𝑓⟩ ∈ 𝑠 → 𝑒 ∈ dom 𝑠)
103	102	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → 𝑒 ∈ dom 𝑠)
104	103	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → 𝑒 ∈ dom 𝑠)
105	98, 100, 104	rspcdva 3613	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ 𝑒𝑅𝑎)
106		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → 𝑒 ≠ 𝑎)
107	106	neneqd 2944	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ 𝑒 = 𝑎)
108		ioran 981	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ↔ (¬ 𝑒𝑅𝑎 ∧ ¬ 𝑒 = 𝑎))
109	105, 107, 108	sylanbrc 582	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎))
110	109	intn3an1d 1478	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
111	96, 110	pm2.61dane 3028	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
112	111	intn3an3d 1480	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
113		eleq1 2820	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞 ∈ 𝑠 ↔ ⟨𝑒, 𝑓⟩ ∈ 𝑠))
114	113	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠)))
115		breq1 5151	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ⟨𝑒, 𝑓⟩𝑇⟨𝑎, 𝑐⟩))
116		xpord2.1	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
117	116	xpord2lem 8133	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑒, 𝑓⟩𝑇⟨𝑎, 𝑐⟩ ↔ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
118	115, 117	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
119	118	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (¬ 𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
120	114, 119	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))))
121	112, 120	mpbiri 258	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
122	121	com12 32	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → (𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
123	122	exlimdvv 1936	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
124	63, 123	mpd 15	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩)
125	124	ralrimiva 3145	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩)
126		breq2 5152	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (𝑞𝑇𝑝 ↔ 𝑞𝑇⟨𝑎, 𝑐⟩))
127	126	notbid 318	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (¬ 𝑞𝑇𝑝 ↔ ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
128	127	ralbidv 3176	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝 ↔ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
129	128	rspcev 3612	. . . . . . 7 ⊢ ((⟨𝑎, 𝑐⟩ ∈ 𝑠 ∧ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
130	60, 125, 129	syl2anc 583	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
131	55, 130	rexlimddv 3160	. . . . 5 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
132	28, 131	rexlimddv 3160	. . . 4 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
133	132	ex 412	. . 3 ⊢ (𝜑 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
134	133	alrimiv 1929	. 2 ⊢ (𝜑 → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
135		df-fr 5631	. 2 ⊢ (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
136	134, 135	sylibr 233	1 ⊢ (𝜑 → 𝑇 Fr (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 844 ∧ w3a 1086 ∀wal 1538 = wceq 1540 ∃wex 1780 ∈ wcel 2105 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 {csn 4628 ⟨cop 4634 class class class wbr 5148 {copab 5210 Fr wfr 5628 × cxp 5674 dom cdm 5676 ran crn 5677 “ cima 5679 Rel wrel 5681 ‘cfv 6543 1^st c1st 7977 2^nd c2nd 7978

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 ax-un 7729

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-fr 5631 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fv 6551 df-1st 7979 df-2nd 7980

This theorem is referenced by: xpord2indlem 8138 on2recsfn 8672 on2recsov 8673 noxpordfr 27781

W3C validator