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 8136

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 5892	. . . . . . . 8 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
2	1	ad2antrl 740	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
3		dmxpss 6169	. . . . . . 7 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
4	2, 3	sstrdi 3949	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ 𝐴)
5		simprr 784	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑠 ≠ ∅)
6		relxp 5679	. . . . . . . . . . 11 ⊢ Rel (𝐴 × 𝐵)
7		relss 5768	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
8	6, 7	mpi 21	. . . . . . . . . 10 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
9	8	ad2antrl 740	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → Rel 𝑠)
10		reldm0 5918	. . . . . . . . 9 ⊢ (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
11	9, 10	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
12	11	necon3bid 3002	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
13	5, 12	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ≠ ∅)
14		frxp2.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 Fr 𝐴)
15	14	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑅 Fr 𝐴)
16		df-fr 5614	. . . . . . . 8 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎))
17	15, 16	sylib 221	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎))
18		vex 3459	. . . . . . . . 9 ⊢ 𝑠 ∈ V
19	18	dmex 7902	. . . . . . . 8 ⊢ dom 𝑠 ∈ V
20		sseq1 3962	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (𝑐 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴))
21		neeq1 3020	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (𝑐 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
22	20, 21	anbi12d 643	. . . . . . . . 9 ⊢ (𝑐 = dom 𝑠 → ((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) ↔ (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅)))
23		raleq 3320	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎 ↔ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
24	23	rexeqbi1dv 3334	. . . . . . . . 9 ⊢ (𝑐 = dom 𝑠 → (∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
25	22, 24	imbi12d 347	. . . . . . . 8 ⊢ (𝑐 = dom 𝑠 → (((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎) ↔ ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)))
26	19, 25	spcv 3564	. . . . . . 7 ⊢ (∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
27	17, 26	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
28	4, 13, 27	mp2and 711	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
29		imassrn 6073	. . . . . . . 8 ⊢ (𝑠 “ {𝑎}) ⊆ ran 𝑠
30		rnss 5929	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
31	30	ad2antrl 740	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
32	31	adantr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
33		rnxpss 6170	. . . . . . . . 9 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
34	32, 33	sstrdi 3949	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠 ⊆ 𝐵)
35	29, 34	sstrid 3948	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ⊆ 𝐵)
36		simprl 782	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → 𝑎 ∈ dom 𝑠)
37		imadisj 6082	. . . . . . . . . 10 ⊢ ((𝑠 “ {𝑎}) = ∅ ↔ (dom 𝑠 ∩ {𝑎}) = ∅)
38		disjsn 4677	. . . . . . . . . 10 ⊢ ((dom 𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
39	37, 38	bitri 278	. . . . . . . . 9 ⊢ ((𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
40	39	necon2abii 3008	. . . . . . . 8 ⊢ (𝑎 ∈ dom 𝑠 ↔ (𝑠 “ {𝑎}) ≠ ∅)
41	36, 40	sylib 221	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ≠ ∅)
42		frxp2.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 Fr 𝐵)
43		df-fr 5614	. . . . . . . . . 10 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
44	42, 43	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
45	44	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
46	18	imaex 7907	. . . . . . . . 9 ⊢ (𝑠 “ {𝑎}) ∈ V
47		sseq1 3962	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (𝑒 ⊆ 𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
48		neeq1 3020	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (𝑒 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
49	47, 48	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑒 = (𝑠 “ {𝑎}) → ((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
50		raleq 3320	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
51	50	rexeqbi1dv 3334	. . . . . . . . . 10 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐 ↔ ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
52	49, 51	imbi12d 347	. . . . . . . . 9 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)))
53	46, 52	spcv 3564	. . . . . . . 8 ⊢ (∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
54	45, 53	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
55	35, 41, 54	mp2and 711	. . . . . 6 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
56		breq2 5113	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (𝑞𝑇𝑝 ↔ 𝑞𝑇⟨𝑎, 𝑐⟩))
57	56	notbid 321	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (¬ 𝑞𝑇𝑝 ↔ ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
58	57	ralbidv 3188	. . . . . . 7 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝 ↔ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
59		simprl 782	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → 𝑐 ∈ (𝑠 “ {𝑎}))
60		vex 3459	. . . . . . . . 9 ⊢ 𝑎 ∈ V
61		vex 3459	. . . . . . . . 9 ⊢ 𝑐 ∈ V
62	60, 61	elimasn 6092	. . . . . . . 8 ⊢ (𝑐 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑐⟩ ∈ 𝑠)
63	59, 62	sylib 221	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ⟨𝑎, 𝑐⟩ ∈ 𝑠)
64	9	ad2antrr 738	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → Rel 𝑠)
65		elrel 5784	. . . . . . . . . 10 ⊢ ((Rel 𝑠 ∧ 𝑞 ∈ 𝑠) → ∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
66	64, 65	sylan 591	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
67		breq1 5112	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑓 → (𝑑𝑆𝑐 ↔ 𝑓𝑆𝑐))
68	67	notbid 321	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑓 → (¬ 𝑑𝑆𝑐 ↔ ¬ 𝑓𝑆𝑐))
69		simplrr 789	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
70		vex 3459	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑓 ∈ V
71	60, 70	elimasn 6092	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠)
72	71	bilanri 511	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → 𝑓 ∈ (𝑠 “ {𝑎}))
73	68, 69, 72	rspcdva 3582	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ 𝑓𝑆𝑐)
74	73	intnanrd 494	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))
75		opeq1 4838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑎 → ⟨𝑒, 𝑓⟩ = ⟨𝑎, 𝑓⟩)
76	75	eleq1d 2848	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑎 → (⟨𝑒, 𝑓⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠))
77	76	anbi2d 641	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠)))
78		3anass 1111	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
79		olc 881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑎 → (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎))
80	79	biantrurd 541	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
81		neeq1 3020	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = 𝑎 → (𝑒 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
82	81	orbi1d 929	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑒 = 𝑎 → ((𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
83		neirr 2967	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ 𝑎 ≠ 𝑎
84	83	biorfi 951	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ≠ 𝑐 ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))
85	82, 84	bitr4di 292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = 𝑎 → ((𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐) ↔ 𝑓 ≠ 𝑐))
86	85	anbi2d 641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐)))
87		andir 1026	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐) ↔ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ∨ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)))
88		nonconne 2970	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ¬ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)
89	88	biorfri 952	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ↔ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ∨ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)))
90	87, 89	bitr4i 281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))
91	86, 90	bitrdi 290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
92	80, 91	bitr3d 284	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑎 → (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
93	78, 92	bitrid 286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑎 → (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
94	93	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑎 → (¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
95	77, 94	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))))
96	74, 95	mpbiri 261	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
97	96	impcom 412	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 = 𝑎) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
98		breq1 5112	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑒 → (𝑏𝑅𝑎 ↔ 𝑒𝑅𝑎))
99	98	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑒 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑒𝑅𝑎))
100		simplrr 789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
101	100	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
102		vex 3459	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑒 ∈ V
103	102, 70	opeldm 5897	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑒, 𝑓⟩ ∈ 𝑠 → 𝑒 ∈ dom 𝑠)
104	103	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → 𝑒 ∈ dom 𝑠)
105	104	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → 𝑒 ∈ dom 𝑠)
106	99, 101, 105	rspcdva 3582	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ 𝑒𝑅𝑎)
107		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → 𝑒 ≠ 𝑎)
108	107	neneqd 2963	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ 𝑒 = 𝑎)
109		ioran 999	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ↔ (¬ 𝑒𝑅𝑎 ∧ ¬ 𝑒 = 𝑎))
110	106, 108, 109	sylanbrc 594	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎))
111	110	intn3an1d 1510	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
112	97, 111	pm2.61dane 3045	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
113	112	intn3an3d 1512	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
114		eleq1 2851	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞 ∈ 𝑠 ↔ ⟨𝑒, 𝑓⟩ ∈ 𝑠))
115	114	anbi2d 641	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠)))
116		breq1 5112	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ⟨𝑒, 𝑓⟩𝑇⟨𝑎, 𝑐⟩))
117		xpord2.1	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
118	117	xpord2lem 8134	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑒, 𝑓⟩𝑇⟨𝑎, 𝑐⟩ ↔ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
119	116, 118	bitrdi 290	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
120	119	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (¬ 𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
121	115, 120	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))))
122	113, 121	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
123	122	com12 33	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → (𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
124	123	exlimdvv 1964	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
125	66, 124	mpd 16	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩)
126	125	ralrimiva 3157	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩)
127	58, 63, 126	rspcedvdw 3584	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
128	55, 127	rexlimddv 3172	. . . . 5 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
129	28, 128	rexlimddv 3172	. . . 4 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
130	129	ex 417	. . 3 ⊢ (𝜑 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
131	130	alrimiv 1957	. 2 ⊢ (𝜑 → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
132		df-fr 5614	. 2 ⊢ (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
133	131, 132	sylibr 237	1 ⊢ (𝜑 → 𝑇 Fr (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1103 ∀wal 1568 = wceq 1570 ∃wex 1809 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 {csn 4589 ⟨cop 4595 class class class wbr 5109 {copab 5173 Fr wfr 5611 × cxp 5659 dom cdm 5661 ran crn 5662 “ cima 5664 Rel wrel 5666 ‘cfv 6536 1^st c1st 7980 2^nd c2nd 7981

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pr 5404 ax-un 7732

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rab 3417 df-v 3457 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-br 5110 df-opab 5174 df-mpt 5193 df-id 5556 df-fr 5614 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-iota 6492 df-fun 6538 df-fv 6544 df-1st 7982 df-2nd 7983

This theorem is referenced by: xpord2indlem 8139 on2recsfn 8649 on2recsov 8650 noxpordfr 28144

W3C validator