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 8076

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 5858	. . . . . . . 8 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
2	1	ad2antrl 726	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
3		dmxpss 6123	. . . . . . 7 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
4	2, 3	sstrdi 3956	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ 𝐴)
5		simprr 771	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑠 ≠ ∅)
6		relxp 5651	. . . . . . . . . . 11 ⊢ Rel (𝐴 × 𝐵)
7		relss 5737	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
8	6, 7	mpi 20	. . . . . . . . . 10 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
9	8	ad2antrl 726	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → Rel 𝑠)
10		reldm0 5883	. . . . . . . . 9 ⊢ (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
11	9, 10	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
12	11	necon3bid 2988	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
13	5, 12	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ≠ ∅)
14		frxp2.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 Fr 𝐴)
15	14	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → 𝑅 Fr 𝐴)
16		df-fr 5588	. . . . . . . 8 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎))
17	15, 16	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎))
18		vex 3449	. . . . . . . . 9 ⊢ 𝑠 ∈ V
19	18	dmex 7848	. . . . . . . 8 ⊢ dom 𝑠 ∈ V
20		sseq1 3969	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (𝑐 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴))
21		neeq1 3006	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (𝑐 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
22	20, 21	anbi12d 631	. . . . . . . . 9 ⊢ (𝑐 = dom 𝑠 → ((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) ↔ (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅)))
23		raleq 3309	. . . . . . . . . 10 ⊢ (𝑐 = dom 𝑠 → (∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎 ↔ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
24	23	rexeqbi1dv 3308	. . . . . . . . 9 ⊢ (𝑐 = dom 𝑠 → (∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
25	22, 24	imbi12d 344	. . . . . . . 8 ⊢ (𝑐 = dom 𝑠 → (((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎) ↔ ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)))
26	19, 25	spcv 3564	. . . . . . 7 ⊢ (∀𝑐((𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅) → ∃𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑐 ¬ 𝑏𝑅𝑎) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
27	17, 26	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎))
28	4, 13, 27	mp2and 697	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom 𝑠∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
29		imassrn 6024	. . . . . . . 8 ⊢ (𝑠 “ {𝑎}) ⊆ ran 𝑠
30		rnss 5894	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
31	30	ad2antrl 726	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
32	31	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
33		rnxpss 6124	. . . . . . . . 9 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
34	32, 33	sstrdi 3956	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ran 𝑠 ⊆ 𝐵)
35	29, 34	sstrid 3955	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ⊆ 𝐵)
36		simprl 769	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → 𝑎 ∈ dom 𝑠)
37		imadisj 6032	. . . . . . . . . 10 ⊢ ((𝑠 “ {𝑎}) = ∅ ↔ (dom 𝑠 ∩ {𝑎}) = ∅)
38		disjsn 4672	. . . . . . . . . 10 ⊢ ((dom 𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
39	37, 38	bitri 274	. . . . . . . . 9 ⊢ ((𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠)
40	39	necon2abii 2994	. . . . . . . 8 ⊢ (𝑎 ∈ dom 𝑠 ↔ (𝑠 “ {𝑎}) ≠ ∅)
41	36, 40	sylib 217	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (𝑠 “ {𝑎}) ≠ ∅)
42		frxp2.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 Fr 𝐵)
43		df-fr 5588	. . . . . . . . . 10 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
44	42, 43	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
45	44	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐))
46	18	imaex 7853	. . . . . . . . 9 ⊢ (𝑠 “ {𝑎}) ∈ V
47		sseq1 3969	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (𝑒 ⊆ 𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
48		neeq1 3006	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (𝑒 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
49	47, 48	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑒 = (𝑠 “ {𝑎}) → ((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
50		raleq 3309	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
51	50	rexeqbi1dv 3308	. . . . . . . . . 10 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐 ↔ ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
52	49, 51	imbi12d 344	. . . . . . . . 9 ⊢ (𝑒 = (𝑠 “ {𝑎}) → (((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)))
53	46, 52	spcv 3564	. . . . . . . 8 ⊢ (∀𝑒((𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅) → ∃𝑐 ∈ 𝑒 ∀𝑑 ∈ 𝑒 ¬ 𝑑𝑆𝑐) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
54	45, 53	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐))
55	35, 41, 54	mp2and 697	. . . . . 6 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑐 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
56		simprl 769	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → 𝑐 ∈ (𝑠 “ {𝑎}))
57		vex 3449	. . . . . . . . 9 ⊢ 𝑎 ∈ V
58		vex 3449	. . . . . . . . 9 ⊢ 𝑐 ∈ V
59	57, 58	elimasn 6041	. . . . . . . 8 ⊢ (𝑐 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑐⟩ ∈ 𝑠)
60	56, 59	sylib 217	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ⟨𝑎, 𝑐⟩ ∈ 𝑠)
61	9	ad2antrr 724	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → Rel 𝑠)
62		elrel 5754	. . . . . . . . . 10 ⊢ ((Rel 𝑠 ∧ 𝑞 ∈ 𝑠) → ∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
63	61, 62	sylan 580	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩)
64		breq1 5108	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑓 → (𝑑𝑆𝑐 ↔ 𝑓𝑆𝑐))
65	64	notbid 317	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑓 → (¬ 𝑑𝑆𝑐 ↔ ¬ 𝑓𝑆𝑐))
66		simplrr 776	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)
67		vex 3449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑓 ∈ V
68	57, 67	elimasn 6041	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠)
69	68	biimpri 227	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑎, 𝑓⟩ ∈ 𝑠 → 𝑓 ∈ (𝑠 “ {𝑎}))
70	69	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → 𝑓 ∈ (𝑠 “ {𝑎}))
71	65, 66, 70	rspcdva 3582	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ 𝑓𝑆𝑐)
72	71	intnanrd 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))
73		opeq1 4830	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑎 → ⟨𝑒, 𝑓⟩ = ⟨𝑎, 𝑓⟩)
74	73	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑎 → (⟨𝑒, 𝑓⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑓⟩ ∈ 𝑠))
75	74	anbi2d 629	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠)))
76		3anass 1095	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
77		olc 866	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑎 → (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎))
78	77	biantrurd 533	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
79		neeq1 3006	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = 𝑎 → (𝑒 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
80	79	orbi1d 915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑒 = 𝑎 → ((𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
81		neirr 2952	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ 𝑎 ≠ 𝑎
82		biorf 935	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑎 ≠ 𝑎 → (𝑓 ≠ 𝑐 ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
83	81, 82	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ≠ 𝑐 ↔ (𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))
84	80, 83	bitr4di 288	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = 𝑎 → ((𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐) ↔ 𝑓 ≠ 𝑐))
85	84	anbi2d 629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐)))
86		andir 1007	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐) ↔ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ∨ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)))
87		nonconne 2955	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ¬ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)
88	87	biorfi 937	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ↔ ((𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐) ∨ (𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐)))
89	86, 88	bitr4i 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ 𝑓 ≠ 𝑐) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))
90	85, 89	bitrdi 286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑎 → (((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
91	78, 90	bitr3d 280	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑎 → (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ ((𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
92	76, 91	bitrid 282	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑎 → (((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
93	92	notbid 317	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑎 → (¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)) ↔ ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐)))
94	75, 93	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑎, 𝑓⟩ ∈ 𝑠) → ¬ (𝑓𝑆𝑐 ∧ 𝑓 ≠ 𝑐))))
95	72, 94	mpbiri 257	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = 𝑎 → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
96	95	impcom 408	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 = 𝑎) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
97		breq1 5108	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑒 → (𝑏𝑅𝑎 ↔ 𝑒𝑅𝑎))
98	97	notbid 317	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑒 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑒𝑅𝑎))
99		simplrr 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
100	99	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)
101		vex 3449	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑒 ∈ V
102	101, 67	opeldm 5863	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑒, 𝑓⟩ ∈ 𝑠 → 𝑒 ∈ dom 𝑠)
103	102	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → 𝑒 ∈ dom 𝑠)
104	103	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → 𝑒 ∈ dom 𝑠)
105	98, 100, 104	rspcdva 3582	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ 𝑒𝑅𝑎)
106		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → 𝑒 ≠ 𝑎)
107	106	neneqd 2948	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ 𝑒 = 𝑎)
108		ioran 982	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ↔ (¬ 𝑒𝑅𝑎 ∧ ¬ 𝑒 = 𝑎))
109	105, 107, 108	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ (𝑒𝑅𝑎 ∨ 𝑒 = 𝑎))
110	109	intn3an1d 1479	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) ∧ 𝑒 ≠ 𝑎) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
111	96, 110	pm2.61dane 3032	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))
112	111	intn3an3d 1481	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
113		eleq1 2825	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞 ∈ 𝑠 ↔ ⟨𝑒, 𝑓⟩ ∈ 𝑠))
114	113	anbi2d 629	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) ↔ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠)))
115		breq1 5108	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ⟨𝑒, 𝑓⟩𝑇⟨𝑎, 𝑐⟩))
116		xpord2.1	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
117	116	xpord2lem 8074	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑒, 𝑓⟩𝑇⟨𝑎, 𝑐⟩ ↔ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))
118	115, 117	bitrdi 286	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
119	118	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (¬ 𝑞𝑇⟨𝑎, 𝑐⟩ ↔ ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐)))))
120	114, 119	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → ((((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩) ↔ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ ⟨𝑒, 𝑓⟩ ∈ 𝑠) → ¬ ((𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵) ∧ ((𝑒𝑅𝑎 ∨ 𝑒 = 𝑎) ∧ (𝑓𝑆𝑐 ∨ 𝑓 = 𝑐) ∧ (𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐))))))
121	112, 120	mpbiri 257	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑒, 𝑓⟩ → (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
122	121	com12 32	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → (𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
123	122	exlimdvv 1937	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑒∃𝑓 𝑞 = ⟨𝑒, 𝑓⟩ → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
124	63, 123	mpd 15	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑇⟨𝑎, 𝑐⟩)
125	124	ralrimiva 3143	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩)
126		breq2 5109	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (𝑞𝑇𝑝 ↔ 𝑞𝑇⟨𝑎, 𝑐⟩))
127	126	notbid 317	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (¬ 𝑞𝑇𝑝 ↔ ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
128	127	ralbidv 3174	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑐⟩ → (∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝 ↔ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩))
129	128	rspcev 3581	. . . . . . 7 ⊢ ((⟨𝑎, 𝑐⟩ ∈ 𝑠 ∧ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇⟨𝑎, 𝑐⟩) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
130	60, 125, 129	syl2anc 584	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) ∧ (𝑐 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑐)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
131	55, 130	rexlimddv 3158	. . . . 5 ⊢ (((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom 𝑠 ∧ ∀𝑏 ∈ dom 𝑠 ¬ 𝑏𝑅𝑎)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
132	28, 131	rexlimddv 3158	. . . 4 ⊢ ((𝜑 ∧ (𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝)
133	132	ex 413	. . 3 ⊢ (𝜑 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
134	133	alrimiv 1930	. 2 ⊢ (𝜑 → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
135		df-fr 5588	. 2 ⊢ (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑇𝑝))
136	134, 135	sylibr 233	1 ⊢ (𝜑 → 𝑇 Fr (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 ∀wal 1539 = wceq 1541 ∃wex 1781 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 {csn 4586 ⟨cop 4592 class class class wbr 5105 {copab 5167 Fr wfr 5585 × cxp 5631 dom cdm 5633 ran crn 5634 “ cima 5636 Rel wrel 5638 ‘cfv 6496 1^st c1st 7919 2^nd c2nd 7920

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 ax-un 7672

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-fr 5588 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-iota 6448 df-fun 6498 df-fv 6504 df-1st 7921 df-2nd 7922

This theorem is referenced by: xpord2indlem 8079 on2recsfn 8613 on2recsov 8614 noxpordfr 27263

W3C validator