frxp3 - Mathbox for Scott Fenton

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

Theorem frxp3 33364

Description: Give foundedness over a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024.)

**Hypotheses**
Ref	Expression
xpord3.1	⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1^st ‘(1^st ‘𝑥))𝑅(1^st ‘(1^st ‘𝑦)) ∨ (1^st ‘(1^st ‘𝑥)) = (1^st ‘(1^st ‘𝑦))) ∧ ((2^nd ‘(1^st ‘𝑥))𝑆(2^nd ‘(1^st ‘𝑦)) ∨ (2^nd ‘(1^st ‘𝑥)) = (2^nd ‘(1^st ‘𝑦))) ∧ ((2^nd ‘𝑥)𝑇(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
frxp3.1	⊢ (𝜑 → 𝑅 Fr 𝐴)
frxp3.2	⊢ (𝜑 → 𝑆 Fr 𝐵)
frxp3.3	⊢ (𝜑 → 𝑇 Fr 𝐶)

**Assertion**
Ref	Expression
frxp3	⊢ (𝜑 → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶))

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦 𝑥,𝐶,𝑦 𝑥,𝑅,𝑦 𝑥,𝑆,𝑦 𝑥,𝑇,𝑦 Allowed substitution hints: 𝜑(𝑥,𝑦) 𝑈(𝑥,𝑦)

Proof of Theorem frxp3 Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 𝑝 𝑞 𝑠 ℎ 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmss 5748	. . . . . . . . . 10 ⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
2	1	ad2antrl 727	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
3		dmxpss 6005	. . . . . . . . 9 ⊢ dom ((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵)
4	2, 3	sstrdi 3906	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ (𝐴 × 𝐵))
5		dmss 5748	. . . . . . . 8 ⊢ (dom 𝑠 ⊆ (𝐴 × 𝐵) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
6	4, 5	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
7		dmxpss 6005	. . . . . . 7 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
8	6, 7	sstrdi 3906	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ 𝐴)
9		simprr 772	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑠 ≠ ∅)
10		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
11		relxp 5546	. . . . . . . . . . 11 ⊢ Rel ((𝐴 × 𝐵) × 𝐶)
12		relss 5630	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → (Rel ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠))
13	10, 11, 12	mpisyl 21	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → Rel 𝑠)
14		reldm0 5774	. . . . . . . . . 10 ⊢ (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
15	13, 14	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
16	15	necon3bid 2995	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
17	9, 16	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ≠ ∅)
18		relxp 5546	. . . . . . . . . 10 ⊢ Rel (𝐴 × 𝐵)
19		relss 5630	. . . . . . . . . 10 ⊢ (dom 𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel dom 𝑠))
20	4, 18, 19	mpisyl 21	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → Rel dom 𝑠)
21		reldm0 5774	. . . . . . . . 9 ⊢ (Rel dom 𝑠 → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
22	20, 21	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
23	22	necon3bid 2995	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅))
24	17, 23	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ≠ ∅)
25		frxp3.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 Fr 𝐴)
26		df-fr 5487	. . . . . . . . 9 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑔((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎))
27	25, 26	sylib 221	. . . . . . . 8 ⊢ (𝜑 → ∀𝑔((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎))
28	27	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∀𝑔((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎))
29		vex 3413	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
30	29	dmex 7627	. . . . . . . . 9 ⊢ dom 𝑠 ∈ V
31	30	dmex 7627	. . . . . . . 8 ⊢ dom dom 𝑠 ∈ V
32		sseq1 3919	. . . . . . . . . 10 ⊢ (𝑔 = dom dom 𝑠 → (𝑔 ⊆ 𝐴 ↔ dom dom 𝑠 ⊆ 𝐴))
33		neeq1 3013	. . . . . . . . . 10 ⊢ (𝑔 = dom dom 𝑠 → (𝑔 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅))
34	32, 33	anbi12d 633	. . . . . . . . 9 ⊢ (𝑔 = dom dom 𝑠 → ((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) ↔ (dom dom 𝑠 ⊆ 𝐴 ∧ dom dom 𝑠 ≠ ∅)))
35		raleq 3323	. . . . . . . . . 10 ⊢ (𝑔 = dom dom 𝑠 → (∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎 ↔ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎))
36	35	rexeqbi1dv 3322	. . . . . . . . 9 ⊢ (𝑔 = dom dom 𝑠 → (∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎 ↔ ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎))
37	34, 36	imbi12d 348	. . . . . . . 8 ⊢ (𝑔 = dom dom 𝑠 → (((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎) ↔ ((dom dom 𝑠 ⊆ 𝐴 ∧ dom dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)))
38	31, 37	spcv 3526	. . . . . . 7 ⊢ (∀𝑔((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎) → ((dom dom 𝑠 ⊆ 𝐴 ∧ dom dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎))
39	28, 38	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ((dom dom 𝑠 ⊆ 𝐴 ∧ dom dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎))
40	8, 24, 39	mp2and 698	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
41		imassrn 5917	. . . . . . . 8 ⊢ (dom 𝑠 “ {𝑎}) ⊆ ran dom 𝑠
42		rnss 5785	. . . . . . . . . . 11 ⊢ (dom 𝑠 ⊆ (𝐴 × 𝐵) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
43	4, 42	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
44		rnxpss 6006	. . . . . . . . . 10 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
45	43, 44	sstrdi 3906	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ 𝐵)
46	45	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ran dom 𝑠 ⊆ 𝐵)
47	41, 46	sstrid 3905	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ⊆ 𝐵)
48		simprl 770	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑎 ∈ dom dom 𝑠)
49		imadisj 5925	. . . . . . . . . 10 ⊢ ((dom 𝑠 “ {𝑎}) = ∅ ↔ (dom dom 𝑠 ∩ {𝑎}) = ∅)
50		disjsn 4607	. . . . . . . . . 10 ⊢ ((dom dom 𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠)
51	49, 50	bitri 278	. . . . . . . . 9 ⊢ ((dom 𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠)
52	51	necon2abii 3001	. . . . . . . 8 ⊢ (𝑎 ∈ dom dom 𝑠 ↔ (dom 𝑠 “ {𝑎}) ≠ ∅)
53	48, 52	sylib 221	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ≠ ∅)
54		frxp3.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 Fr 𝐵)
55		df-fr 5487	. . . . . . . . . 10 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑔((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏))
56	54, 55	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑔((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏))
57	30	imaex 7632	. . . . . . . . . 10 ⊢ (dom 𝑠 “ {𝑎}) ∈ V
58		sseq1 3919	. . . . . . . . . . . 12 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (𝑔 ⊆ 𝐵 ↔ (dom 𝑠 “ {𝑎}) ⊆ 𝐵))
59		neeq1 3013	. . . . . . . . . . . 12 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (𝑔 ≠ ∅ ↔ (dom 𝑠 “ {𝑎}) ≠ ∅))
60	58, 59	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → ((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) ↔ ((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅)))
61		raleq 3323	. . . . . . . . . . . 12 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏 ↔ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
62	61	rexeqbi1dv 3322	. . . . . . . . . . 11 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏 ↔ ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
63	60, 62	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏) ↔ (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)))
64	57, 63	spcv 3526	. . . . . . . . 9 ⊢ (∀𝑔((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏) → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
65	56, 64	syl 17	. . . . . . . 8 ⊢ (𝜑 → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
66	65	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
67	47, 53, 66	mp2and 698	. . . . . 6 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
68		imassrn 5917	. . . . . . . . . 10 ⊢ (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ ran 𝑠
69		rnss 5785	. . . . . . . . . . . 12 ⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
70	69	ad2antrl 727	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
71		rnxpss 6006	. . . . . . . . . . 11 ⊢ ran ((𝐴 × 𝐵) × 𝐶) ⊆ 𝐶
72	70, 71	sstrdi 3906	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ 𝐶)
73	68, 72	sstrid 3905	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶)
74	73	ad2antrr 725	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶)
75		simprl 770	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 𝑏 ∈ (dom 𝑠 “ {𝑎}))
76		vex 3413	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
77		vex 3413	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
78	76, 77	elimasn 5931	. . . . . . . . . 10 ⊢ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
79	75, 78	sylib 221	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
80		imadisj 5925	. . . . . . . . . . 11 ⊢ ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ (dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅)
81		disjsn 4607	. . . . . . . . . . 11 ⊢ ((dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
82	80, 81	bitri 278	. . . . . . . . . 10 ⊢ ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
83	82	necon2abii 3001	. . . . . . . . 9 ⊢ (⟨𝑎, 𝑏⟩ ∈ dom 𝑠 ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
84	79, 83	sylib 221	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
85		frxp3.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 Fr 𝐶)
86		df-fr 5487	. . . . . . . . . . 11 ⊢ (𝑇 Fr 𝐶 ↔ ∀𝑔((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐))
87	85, 86	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑔((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐))
88	29	imaex 7632	. . . . . . . . . . 11 ⊢ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∈ V
89		sseq1 3919	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (𝑔 ⊆ 𝐶 ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶))
90		neeq1 3013	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (𝑔 ≠ ∅ ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅))
91	89, 90	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → ((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) ↔ ((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)))
92		raleq 3323	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐 ↔ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
93	92	rexeqbi1dv 3322	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐 ↔ ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
94	91, 93	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐) ↔ (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)))
95	88, 94	spcv 3526	. . . . . . . . . 10 ⊢ (∀𝑔((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐) → (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
96	87, 95	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
97	96	ad3antrrr 729	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
98	74, 84, 97	mp2and 698	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
99		simprl 770	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → 𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}))
100		opex 5328	. . . . . . . . . 10 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
101		vex 3413	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
102	100, 101	elimasn 5931	. . . . . . . . 9 ⊢ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
103	99, 102	sylib 221	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
104		simplrl 776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
105	104	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
106		elxpxpss 33215	. . . . . . . . . . 11 ⊢ ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ 𝑠) → ∃𝑔∃ℎ∃𝑖 𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩)
107	105, 106	sylan 583	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ∃𝑔∃ℎ∃𝑖 𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩)
108		df-ne 2952	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ≠ 𝑐 ↔ ¬ 𝑖 = 𝑐)
109	108	con2bii 361	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑐 ↔ ¬ 𝑖 ≠ 𝑐)
110	109	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑐 → ¬ 𝑖 ≠ 𝑐)
111	110	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ 𝑖 ≠ 𝑐)
112	111	intnand 492	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))
113		breq1 5039	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑖 → (𝑓𝑇𝑐 ↔ 𝑖𝑇𝑐))
114	113	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑖 → (¬ 𝑓𝑇𝑐 ↔ ¬ 𝑖𝑇𝑐))
115		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
116	115	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
117		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
118		vex 3413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑖 ∈ V
119	100, 118	elimasn 5931	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
120	117, 119	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}))
121	114, 116, 120	rspcdva 3545	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ 𝑖𝑇𝑐)
122		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐)
123	122	neneqd 2956	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ 𝑖 = 𝑐)
124		ioran 981	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐) ↔ (¬ 𝑖𝑇𝑐 ∧ ¬ 𝑖 = 𝑐))
125	121, 123, 124	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐))
126	125	intn3an3d 1478	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)))
127	126	intnanrd 493	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))
128	112, 127	pm2.61dane 3038	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))
129		opeq2 4766	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = 𝑏 → ⟨𝑎, ℎ⟩ = ⟨𝑎, 𝑏⟩)
130	129	opeq1d 4772	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑏 → ⟨⟨𝑎, ℎ⟩, 𝑖⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑖⟩)
131	130	eleq1d 2836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑏 → (⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠 ↔ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠))
132	131	anbi2d 631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)))
133		neeq1 3013	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = 𝑏 → (ℎ ≠ 𝑏 ↔ 𝑏 ≠ 𝑏))
134	133	orbi1d 914	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = 𝑏 → ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
135		neirr 2960	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ¬ 𝑏 ≠ 𝑏
136		orel1 886	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑏 ≠ 𝑏 → ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐))
137	135, 136	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐)
138		olc 865	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ≠ 𝑐 → (𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))
139	137, 138	impbii 212	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ 𝑖 ≠ 𝑐)
140	134, 139	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑏 → ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ 𝑖 ≠ 𝑐))
141	140	anbi2d 631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑏 → ((((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)))
142	141	notbid 321	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑏 → (¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)))
143	132, 142	imbi12d 348	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ = 𝑏 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))))
144	128, 143	mpbiri 261	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
145	144	impcom 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ = 𝑏) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
146		breq1 5039	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = ℎ → (𝑒𝑆𝑏 ↔ ℎ𝑆𝑏))
147	146	notbid 321	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑒 = ℎ → (¬ 𝑒𝑆𝑏 ↔ ¬ ℎ𝑆𝑏))
148		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
149	148	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
150		opex 5328	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ⟨𝑎, ℎ⟩ ∈ V
151	150, 118	opeldm 5753	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑎, ℎ⟩ ∈ dom 𝑠)
152	151	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ⟨𝑎, ℎ⟩ ∈ dom 𝑠)
153	152	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ⟨𝑎, ℎ⟩ ∈ dom 𝑠)
154		vex 3413	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℎ ∈ V
155	76, 154	elimasn 5931	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, ℎ⟩ ∈ dom 𝑠)
156	153, 155	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ℎ ∈ (dom 𝑠 “ {𝑎}))
157	147, 149, 156	rspcdva 3545	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ℎ𝑆𝑏)
158		simpr 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ℎ ≠ 𝑏)
159	158	neneqd 2956	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ℎ = 𝑏)
160		ioran 981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ↔ (¬ ℎ𝑆𝑏 ∧ ¬ ℎ = 𝑏))
161	157, 159, 160	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ (ℎ𝑆𝑏 ∨ ℎ = 𝑏))
162	161	intn3an2d 1477	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)))
163	162	intnanrd 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
164	145, 163	pm2.61dane 3038	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
165		opeq1 4764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = 𝑎 → ⟨𝑔, ℎ⟩ = ⟨𝑎, ℎ⟩)
166	165	opeq1d 4772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑎 → ⟨⟨𝑔, ℎ⟩, 𝑖⟩ = ⟨⟨𝑎, ℎ⟩, 𝑖⟩)
167	166	eleq1d 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑎 → (⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠 ↔ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠))
168	167	anbi2d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠)))
169		3orass 1087	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑔 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
170		neeq1 3013	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 = 𝑎 → (𝑔 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
171	170	orbi1d 914	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
172	169, 171	syl5bb 286	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
173		neirr 2960	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ 𝑎 ≠ 𝑎
174		orel1 886	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑎 ≠ 𝑎 → ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) → (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
175	173, 174	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) → (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))
176		olc 865	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
177	175, 176	impbii 212	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))
178	172, 177	bitrdi 290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
179	178	anbi2d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑎 → ((((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
180	179	notbid 321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑎 → (¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
181	168, 180	imbi12d 348	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑎 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))))
182	164, 181	mpbiri 261	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
183	182	impcom 411	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 = 𝑎) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
184		breq1 5039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑔 → (𝑑𝑅𝑎 ↔ 𝑔𝑅𝑎))
185	184	notbid 321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑔 → (¬ 𝑑𝑅𝑎 ↔ ¬ 𝑔𝑅𝑎))
186		simplrr 777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
187	186	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
188		opex 5328	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ⟨𝑔, ℎ⟩ ∈ V
189	188, 118	opeldm 5753	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑔, ℎ⟩ ∈ dom 𝑠)
190	189	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ⟨𝑔, ℎ⟩ ∈ dom 𝑠)
191		vex 3413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑔 ∈ V
192	191, 154	opeldm 5753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑔, ℎ⟩ ∈ dom 𝑠 → 𝑔 ∈ dom dom 𝑠)
193	190, 192	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → 𝑔 ∈ dom dom 𝑠)
194	193	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 𝑔 ∈ dom dom 𝑠)
195	185, 187, 194	rspcdva 3545	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ 𝑔𝑅𝑎)
196		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 𝑔 ≠ 𝑎)
197	196	neneqd 2956	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ 𝑔 = 𝑎)
198		ioran 981	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ↔ (¬ 𝑔𝑅𝑎 ∧ ¬ 𝑔 = 𝑎))
199	195, 197, 198	sylanbrc 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ (𝑔𝑅𝑎 ∨ 𝑔 = 𝑎))
200	199	intn3an1d 1476	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)))
201	200	intnanrd 493	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
202	183, 201	pm2.61dane 3038	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
203	202	intn3an3d 1478	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
204		eleq1 2839	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → (𝑞 ∈ 𝑠 ↔ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠))
205	204	anbi2d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠)))
206		breq1 5039	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ⟨⟨𝑔, ℎ⟩, 𝑖⟩𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
207		xpord3.1	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1^st ‘(1^st ‘𝑥))𝑅(1^st ‘(1^st ‘𝑦)) ∨ (1^st ‘(1^st ‘𝑥)) = (1^st ‘(1^st ‘𝑦))) ∧ ((2^nd ‘(1^st ‘𝑥))𝑆(2^nd ‘(1^st ‘𝑦)) ∨ (2^nd ‘(1^st ‘𝑥)) = (2^nd ‘(1^st ‘𝑦))) ∧ ((2^nd ‘𝑥)𝑇(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
208	207	xpord3lem 33362	. . . . . . . . . . . . . . . . 17 ⊢ (⟨⟨𝑔, ℎ⟩, 𝑖⟩𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
209	206, 208	bitrdi 290	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))))
210	209	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → (¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))))
211	205, 210	imbi12d 348	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))))
212	203, 211	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
213	212	com12 32	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
214	213	exlimdv 1934	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑖 𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
215	214	exlimdvv 1935	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑔∃ℎ∃𝑖 𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
216	107, 215	mpd 15	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩)
217	216	ralrimiva 3113	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩)
218		breq2 5040	. . . . . . . . . . 11 ⊢ (𝑝 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (𝑞𝑈𝑝 ↔ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
219	218	notbid 321	. . . . . . . . . 10 ⊢ (𝑝 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (¬ 𝑞𝑈𝑝 ↔ ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
220	219	ralbidv 3126	. . . . . . . . 9 ⊢ (𝑝 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝 ↔ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
221	220	rspcev 3543	. . . . . . . 8 ⊢ ((⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠 ∧ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
222	103, 217, 221	syl2anc 587	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
223	98, 222	rexlimddv 3215	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
224	67, 223	rexlimddv 3215	. . . . 5 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
225	40, 224	rexlimddv 3215	. . . 4 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
226	225	ex 416	. . 3 ⊢ (𝜑 → ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝))
227	226	alrimiv 1928	. 2 ⊢ (𝜑 → ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝))
228		df-fr 5487	. 2 ⊢ (𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ↔ ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝))
229	227, 228	sylibr 237	1 ⊢ (𝜑 → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∨ w3o 1083 ∧ 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-3or 1085 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-csb 3808 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-iun 4888 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: xpord3ind 33367 no3indslem 33697

W3C validator