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 8086

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 5850	. . . . . . . 8 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
2	1	ad2antrl 735	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
3		dmxpss 6125	. . . . . . 7 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
4	2, 3	sstrdi 3928	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ 𝐴)
5		simprr 779	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑠 ≠ ∅)
6		relxp 5638	. . . . . . . . . . 11 ⊢ Rel (𝐴 × 𝐵)
7		relss 5727	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
8	6, 7	mpi 20	. . . . . . . . . 10 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
9	8	ad2antrl 735	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → Rel 𝑠)
10		reldm0 5876	. . . . . . . . 9 ⊢ (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
11	9, 10	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
12	11	necon3bid 2980	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
13	5, 12	mpbid 234	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ≠ ∅)
14		frxp2.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 Fr 𝐴)
15	14	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑅 Fr 𝐴)
16		df-fr 5573	. . . . . . . 8 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎))
17	15, 16	sylib 220	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎))
18		vex 3437	. . . . . . . . 9 ⊢ 𝑠 ∈ V
19	18	dmex 7853	. . . . . . . 8 ⊢ dom 𝑠 ∈ V
20		sseq1 3941	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (𝑐 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴))
21		neeq1 2998	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (𝑐 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
22	20, 21	anbi12d 639	. . . . . . . . 9 ⊢ (𝑐 = dom 𝑠 → ((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) ↔ (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅)))
23		raleq 3296	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎 ↔ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
24	23	rexeqbi1dv 3310	. . . . . . . . 9 ⊢ (𝑐 = dom 𝑠 → (∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
25	22, 24	imbi12d 346	. . . . . . . 8 ⊢ (𝑐 = dom 𝑠 → (((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎) ↔ ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)))
26	19, 25	spcv 3544	. . . . . . 7 ⊢ (∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
27	17, 26	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
28	4, 13, 27	mp2and 706	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
29		imassrn 6029	. . . . . . . 8 ⊢ (𝑠 “ {𝑎}) ⊆ ran 𝑠
30		rnss 5887	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
31	30	ad2antrl 735	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
32	31	adantr 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
33		rnxpss 6126	. . . . . . . . 9 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
34	32, 33	sstrdi 3928	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠 ⊆ 𝐵)
35	29, 34	sstrid 3927	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ⊆ 𝐵)
36		simprl 777	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → 𝑎 ∈ dom 𝑠)
37		imadisj 6038	. . . . . . . . . 10 ⊢ ((𝑠 “ {𝑎}) = ∅ ↔ (dom 𝑠 ∩ {𝑎}) = ∅)
38		disjsn 4645	. . . . . . . . . 10 ⊢ ((dom 𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
39	37, 38	bitri 277	. . . . . . . . 9 ⊢ ((𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
40	39	necon2abii 2986	. . . . . . . 8 ⊢ (𝑎 ∈ dom 𝑠 ↔ (𝑠 “ {𝑎}) ≠ ∅)
41	36, 40	sylib 220	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ≠ ∅)
42		frxp2.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 Fr 𝐵)
43		df-fr 5573	. . . . . . . . . 10 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
44	42, 43	sylib 220	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
45	44	ad2antrr 733	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
46	18	imaex 7858	. . . . . . . . 9 ⊢ (𝑠 “ {𝑎}) ∈ V
47		sseq1 3941	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (𝑒 ⊆ 𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
48		neeq1 2998	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (𝑒 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
49	47, 48	anbi12d 639	. . . . . . . . . 10 ⊢ (𝑒 = (𝑠 “ {𝑎}) → ((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
50		raleq 3296	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
51	50	rexeqbi1dv 3310	. . . . . . . . . 10 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐 ↔ ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
52	49, 51	imbi12d 346	. . . . . . . . 9 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)))
53	46, 52	spcv 3544	. . . . . . . 8 ⊢ (∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
54	45, 53	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
55	35, 41, 54	mp2and 706	. . . . . 6 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
56		breq2 5078	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (𝑞𝑇𝑝 ↔ 𝑞𝑇⟨𝑎, 𝑐⟩))
57	56	notbid 320	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (¬ 𝑞𝑇𝑝 ↔ ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
58	57	ralbidv 3164	. . . . . . 7 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝 ↔ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
59		simprl 777	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → 𝑐 ∈ (𝑠 “ {𝑎}))
60		vex 3437	. . . . . . . . 9 ⊢ 𝑎 ∈ V
61		vex 3437	. . . . . . . . 9 ⊢ 𝑐 ∈ V
62	60, 61	elimasn 6048	. . . . . . . 8 ⊢ (𝑐 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑐⟩ ∈ 𝑠)
63	59, 62	sylib 220	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ⟨𝑎, 𝑐⟩ ∈ 𝑠)
64	9	ad2antrr 733	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → Rel 𝑠)
65		elrel 5743	. . . . . . . . . 10 ⊢ ((Rel 𝑠 ∧ 𝑞 ∈ 𝑠) → ∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
66	64, 65	sylan 587	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
67		breq1 5077	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑓 → (𝑑𝑆𝑐 ↔ 𝑓𝑆𝑐))
68	67	notbid 320	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑓 → (¬ 𝑑𝑆𝑐 ↔ ¬ 𝑓𝑆𝑐))
69		simplrr 784	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
70		vex 3437	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑓 ∈ V
71	60, 70	elimasn 6048	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠)
72	71	bilanri 508	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → 𝑓 ∈ (𝑠 “ {𝑎}))
73	68, 69, 72	rspcdva 3562	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ 𝑓𝑆𝑐)
74	73	intnanrd 491	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))
75		opeq1 4806	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑎 → ⟨𝑒, 𝑓⟩ = ⟨𝑎, 𝑓⟩)
76	75	eleq1d 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑎 → (⟨𝑒, 𝑓⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠))
77	76	anbi2d 637	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠)))
78		3anass 1101	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
79		olc 875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑎 → (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎))
80	79	biantrurd 538	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
81		neeq1 2998	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = 𝑎 → (𝑒 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
82	81	orbi1d 923	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑒 = 𝑎 → ((𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
83		neirr 2945	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ 𝑎 ≠ 𝑎
84	83	biorfi 945	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ≠ 𝑐 ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))
85	82, 84	bitr4di 291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = 𝑎 → ((𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐) ↔ 𝑓 ≠ 𝑐))
86	85	anbi2d 637	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐)))
87		andir 1017	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐) ↔ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ∨ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)))
88		nonconne 2948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ¬ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)
89	88	biorfri 946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ↔ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ∨ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)))
90	87, 89	bitr4i 280	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))
91	86, 90	bitrdi 289	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
92	80, 91	bitr3d 283	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑎 → (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
93	78, 92	bitrid 285	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑎 → (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
94	93	notbid 320	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑎 → (¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
95	77, 94	imbi12d 346	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))))
96	74, 95	mpbiri 260	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
97	96	impcom 409	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 = 𝑎) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
98		breq1 5077	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑒 → (𝑏𝑅𝑎 ↔ 𝑒𝑅𝑎))
99	98	notbid 320	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑒 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑒𝑅𝑎))
100		simplrr 784	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
101	100	ad2antrr 733	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
102		vex 3437	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑒 ∈ V
103	102, 70	opeldm 5855	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑒, 𝑓⟩ ∈ 𝑠 → 𝑒 ∈ dom 𝑠)
104	103	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → 𝑒 ∈ dom 𝑠)
105	104	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → 𝑒 ∈ dom 𝑠)
106	99, 101, 105	rspcdva 3562	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ 𝑒𝑅𝑎)
107		simpr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → 𝑒 ≠ 𝑎)
108	107	neneqd 2941	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ 𝑒 = 𝑎)
109		ioran 992	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ↔ (¬ 𝑒𝑅𝑎 ∧ ¬ 𝑒 = 𝑎))
110	106, 108, 109	sylanbrc 590	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎))
111	110	intn3an1d 1488	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
112	97, 111	pm2.61dane 3023	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
113	112	intn3an3d 1490	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
114		eleq1 2829	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞 ∈ 𝑠 ↔ ⟨𝑒, 𝑓⟩ ∈ 𝑠))
115	114	anbi2d 637	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠)))
116		breq1 5077	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ⟨𝑒, 𝑓⟩𝑇⟨𝑎, 𝑐⟩))
117		xpord2.1	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
118	117	xpord2lem 8084	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑒, 𝑓⟩𝑇⟨𝑎, 𝑐⟩ ↔ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
119	116, 118	bitrdi 289	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
120	119	notbid 320	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (¬ 𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
121	115, 120	imbi12d 346	. . . . . . . . . . . 12 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))))
122	113, 121	mpbiri 260	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
123	122	com12 32	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → (𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
124	123	exlimdvv 1942	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
125	66, 124	mpd 15	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩)
126	125	ralrimiva 3133	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩)
127	58, 63, 126	rspcedvdw 3564	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
128	55, 127	rexlimddv 3148	. . . . 5 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
129	28, 128	rexlimddv 3148	. . . 4 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
130	129	ex 414	. . 3 ⊢ (𝜑 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
131	130	alrimiv 1935	. 2 ⊢ (𝜑 → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
132		df-fr 5573	. 2 ⊢ (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
133	131, 132	sylibr 236	1 ⊢ (𝜑 → 𝑇 Fr (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 397 ∨ wo 854 ∧ w3a 1093 ∀wal 1546 = wceq 1548 ∃wex 1787 ∈ wcel 2121 ≠ wne 2936 ∀wral 3055 ∃wrex 3065 ∩ cin 3883 ⊆ wss 3884 ∅c0 4263 {csn 4557 ⟨cop 4563 class class class wbr 5074 {copab 5136 Fr wfr 5570 × cxp 5618 dom cdm 5620 ran crn 5621 “ cima 5623 Rel wrel 5625 ‘cfv 6488 1^st c1st 7931 2^nd c2nd 7932

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-sep 5220 ax-nul 5230 ax-pr 5364 ax-un 7681

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-ral 3056 df-rex 3066 df-rab 3394 df-v 3435 df-dif 3887 df-un 3889 df-in 3891 df-ss 3901 df-nul 4264 df-if 4457 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4841 df-br 5075 df-opab 5137 df-mpt 5156 df-id 5515 df-fr 5573 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-iota 6444 df-fun 6490 df-fv 6496 df-1st 7933 df-2nd 7934

This theorem is referenced by: xpord2indlem 8089 on2recsfn 8597 on2recsov 8598 noxpordfr 27963

W3C validator