frxp2 - Mathbox for Scott Fenton

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

Theorem frxp2 33358

Description: Another way of giving a founded order to a cross 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 5748	. . . . . . . 8 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
2	1	ad2antrl 727	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
3		dmxpss 6005	. . . . . . 7 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
4	2, 3	sstrdi 3906	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ 𝐴)
5		simprr 772	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑠 ≠ ∅)
6		relxp 5546	. . . . . . . . . . 11 ⊢ Rel (𝐴 × 𝐵)
7		relss 5630	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
8	6, 7	mpi 20	. . . . . . . . . 10 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
9	8	ad2antrl 727	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → Rel 𝑠)
10		reldm0 5774	. . . . . . . . 9 ⊢ (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
11	9, 10	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
12	11	necon3bid 2995	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
13	5, 12	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ≠ ∅)
14		frxp2.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 Fr 𝐴)
15	14	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑅 Fr 𝐴)
16		df-fr 5487	. . . . . . . 8 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎))
17	15, 16	sylib 221	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎))
18		vex 3413	. . . . . . . . 9 ⊢ 𝑠 ∈ V
19	18	dmex 7627	. . . . . . . 8 ⊢ dom 𝑠 ∈ V
20		sseq1 3919	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (𝑐 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴))
21		neeq1 3013	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (𝑐 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
22	20, 21	anbi12d 633	. . . . . . . . 9 ⊢ (𝑐 = dom 𝑠 → ((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) ↔ (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅)))
23		raleq 3323	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎 ↔ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
24	23	rexeqbi1dv 3322	. . . . . . . . 9 ⊢ (𝑐 = dom 𝑠 → (∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
25	22, 24	imbi12d 348	. . . . . . . 8 ⊢ (𝑐 = dom 𝑠 → (((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎) ↔ ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)))
26	19, 25	spcv 3526	. . . . . . 7 ⊢ (∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
27	17, 26	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
28	4, 13, 27	mp2and 698	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
29		imassrn 5917	. . . . . . . 8 ⊢ (𝑠 “ {𝑎}) ⊆ ran 𝑠
30		rnss 5785	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
31	30	ad2antrl 727	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
32	31	adantr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
33		rnxpss 6006	. . . . . . . . 9 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
34	32, 33	sstrdi 3906	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠 ⊆ 𝐵)
35	29, 34	sstrid 3905	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ⊆ 𝐵)
36		simprl 770	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → 𝑎 ∈ dom 𝑠)
37		imadisj 5925	. . . . . . . . . 10 ⊢ ((𝑠 “ {𝑎}) = ∅ ↔ (dom 𝑠 ∩ {𝑎}) = ∅)
38		disjsn 4607	. . . . . . . . . 10 ⊢ ((dom 𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
39	37, 38	bitri 278	. . . . . . . . 9 ⊢ ((𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
40	39	necon2abii 3001	. . . . . . . 8 ⊢ (𝑎 ∈ dom 𝑠 ↔ (𝑠 “ {𝑎}) ≠ ∅)
41	36, 40	sylib 221	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ≠ ∅)
42		frxp2.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 Fr 𝐵)
43		df-fr 5487	. . . . . . . . . 10 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
44	42, 43	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
45	44	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
46	18	imaex 7632	. . . . . . . . 9 ⊢ (𝑠 “ {𝑎}) ∈ V
47		sseq1 3919	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (𝑒 ⊆ 𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
48		neeq1 3013	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (𝑒 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
49	47, 48	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑒 = (𝑠 “ {𝑎}) → ((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
50		raleq 3323	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
51	50	rexeqbi1dv 3322	. . . . . . . . . 10 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐 ↔ ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
52	49, 51	imbi12d 348	. . . . . . . . 9 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)))
53	46, 52	spcv 3526	. . . . . . . 8 ⊢ (∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
54	45, 53	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
55	35, 41, 54	mp2and 698	. . . . . 6 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
56		simprl 770	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → 𝑐 ∈ (𝑠 “ {𝑎}))
57		vex 3413	. . . . . . . . 9 ⊢ 𝑎 ∈ V
58		vex 3413	. . . . . . . . 9 ⊢ 𝑐 ∈ V
59	57, 58	elimasn 5931	. . . . . . . 8 ⊢ (𝑐 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑐⟩ ∈ 𝑠)
60	56, 59	sylib 221	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ⟨𝑎, 𝑐⟩ ∈ 𝑠)
61	9	ad2antrr 725	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → Rel 𝑠)
62		elrel 5645	. . . . . . . . . 10 ⊢ ((Rel 𝑠 ∧ 𝑞 ∈ 𝑠) → ∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
63	61, 62	sylan 583	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
64		breq1 5039	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑓 → (𝑑𝑆𝑐 ↔ 𝑓𝑆𝑐))
65	64	notbid 321	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑓 → (¬ 𝑑𝑆𝑐 ↔ ¬ 𝑓𝑆𝑐))
66		simplrr 777	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
67		vex 3413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑓 ∈ V
68	57, 67	elimasn 5931	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠)
69	68	biimpri 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑎, 𝑓⟩ ∈ 𝑠 → 𝑓 ∈ (𝑠 “ {𝑎}))
70	69	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → 𝑓 ∈ (𝑠 “ {𝑎}))
71	65, 66, 70	rspcdva 3545	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ 𝑓𝑆𝑐)
72	71	intnanrd 493	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))
73		opeq1 4764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑎 → ⟨𝑒, 𝑓⟩ = ⟨𝑎, 𝑓⟩)
74	73	eleq1d 2836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑎 → (⟨𝑒, 𝑓⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠))
75	74	anbi2d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠)))
76		3anass 1092	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
77		olc 865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑎 → (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎))
78	77	biantrurd 536	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
79		neeq1 3013	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = 𝑎 → (𝑒 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
80	79	orbi1d 914	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑒 = 𝑎 → ((𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
81		neirr 2960	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ 𝑎 ≠ 𝑎
82		biorf 934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑎 ≠ 𝑎 → (𝑓 ≠ 𝑐 ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
83	81, 82	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ≠ 𝑐 ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))
84	80, 83	bitr4di 292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = 𝑎 → ((𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐) ↔ 𝑓 ≠ 𝑐))
85	84	anbi2d 631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐)))
86		andir 1006	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐) ↔ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ∨ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)))
87		nonconne 2963	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ¬ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)
88	87	biorfi 936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ↔ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ∨ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)))
89	86, 88	bitr4i 281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))
90	85, 89	bitrdi 290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
91	78, 90	bitr3d 284	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑎 → (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
92	76, 91	syl5bb 286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑎 → (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
93	92	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑎 → (¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
94	75, 93	imbi12d 348	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))))
95	72, 94	mpbiri 261	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
96	95	impcom 411	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 = 𝑎) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
97		breq1 5039	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑒 → (𝑏𝑅𝑎 ↔ 𝑒𝑅𝑎))
98	97	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑒 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑒𝑅𝑎))
99		simplrr 777	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
100	99	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
101		vex 3413	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑒 ∈ V
102	101, 67	opeldm 5753	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑒, 𝑓⟩ ∈ 𝑠 → 𝑒 ∈ dom 𝑠)
103	102	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → 𝑒 ∈ dom 𝑠)
104	103	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → 𝑒 ∈ dom 𝑠)
105	98, 100, 104	rspcdva 3545	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ 𝑒𝑅𝑎)
106		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → 𝑒 ≠ 𝑎)
107	106	neneqd 2956	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ 𝑒 = 𝑎)
108		ioran 981	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ↔ (¬ 𝑒𝑅𝑎 ∧ ¬ 𝑒 = 𝑎))
109	105, 107, 108	sylanbrc 586	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎))
110	109	intn3an1d 1476	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
111	96, 110	pm2.61dane 3038	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
112	111	intn3an3d 1478	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
113		eleq1 2839	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞 ∈ 𝑠 ↔ ⟨𝑒, 𝑓⟩ ∈ 𝑠))
114	113	anbi2d 631	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠)))
115		breq1 5039	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ⟨𝑒, 𝑓⟩𝑇⟨𝑎, 𝑐⟩))
116		xpord2.1	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
117	116	xpord2lem 33356	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑒, 𝑓⟩𝑇⟨𝑎, 𝑐⟩ ↔ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
118	115, 117	bitrdi 290	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
119	118	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (¬ 𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
120	114, 119	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))))
121	112, 120	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
122	121	com12 32	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → (𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
123	122	exlimdvv 1935	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
124	63, 123	mpd 15	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩)
125	124	ralrimiva 3113	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩)
126		breq2 5040	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (𝑞𝑇𝑝 ↔ 𝑞𝑇⟨𝑎, 𝑐⟩))
127	126	notbid 321	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (¬ 𝑞𝑇𝑝 ↔ ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
128	127	ralbidv 3126	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝 ↔ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
129	128	rspcev 3543	. . . . . . 7 ⊢ ((⟨𝑎, 𝑐⟩ ∈ 𝑠 ∧ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
130	60, 125, 129	syl2anc 587	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
131	55, 130	rexlimddv 3215	. . . . 5 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
132	28, 131	rexlimddv 3215	. . . 4 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
133	132	ex 416	. . 3 ⊢ (𝜑 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
134	133	alrimiv 1928	. 2 ⊢ (𝜑 → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
135		df-fr 5487	. 2 ⊢ (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
136	134, 135	sylibr 237	1 ⊢ (𝜑 → 𝑇 Fr (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∧ w3a 1084 ∀wal 1536 = wceq 1538 ∃wex 1781 ∈ wcel 2111 ≠ wne 2951 ∀wral 3070 ∃wrex 3071 ∩ cin 3859 ⊆ wss 3860 ∅c0 4227 {csn 4525 ⟨cop 4531 class class class wbr 5036 {copab 5098 Fr wfr 5484 × cxp 5526 dom cdm 5528 ran crn 5529 “ cima 5531 Rel wrel 5533 ‘cfv 6340 1^st c1st 7697 2^nd c2nd 7698

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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-sep 5173 ax-nul 5180 ax-pr 5302 ax-un 7465

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-ral 3075 df-rex 3076 df-rab 3079 df-v 3411 df-sbc 3699 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-nul 4228 df-if 4424 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4802 df-br 5037 df-opab 5099 df-mpt 5117 df-id 5434 df-fr 5487 df-xp 5534 df-rel 5535 df-cnv 5536 df-co 5537 df-dm 5538 df-rn 5539 df-res 5540 df-ima 5541 df-iota 6299 df-fun 6342 df-fv 6348 df-1st 7699 df-2nd 7700

This theorem is referenced by: xpord2ind 33361 on2recsfn 33423 on2recsov 33424 noxpordfr 33690

W3C validator