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 33797

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 5811	. . . . . . . . . 10 ⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
2	1	ad2antrl 725	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
3		dmxpss 6074	. . . . . . . . 9 ⊢ dom ((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵)
4	2, 3	sstrdi 3933	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ (𝐴 × 𝐵))
5		dmss 5811	. . . . . . . 8 ⊢ (dom 𝑠 ⊆ (𝐴 × 𝐵) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
6	4, 5	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
7		dmxpss 6074	. . . . . . 7 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
8	6, 7	sstrdi 3933	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ 𝐴)
9		simprr 770	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑠 ≠ ∅)
10		simprl 768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
11		relxp 5607	. . . . . . . . . . 11 ⊢ Rel ((𝐴 × 𝐵) × 𝐶)
12		relss 5692	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → (Rel ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠))
13	10, 11, 12	mpisyl 21	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → Rel 𝑠)
14		reldm0 5837	. . . . . . . . . 10 ⊢ (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
15	13, 14	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
16	15	necon3bid 2988	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
17	9, 16	mpbid 231	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ≠ ∅)
18		relxp 5607	. . . . . . . . . 10 ⊢ Rel (𝐴 × 𝐵)
19		relss 5692	. . . . . . . . . 10 ⊢ (dom 𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel dom 𝑠))
20	4, 18, 19	mpisyl 21	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → Rel dom 𝑠)
21		reldm0 5837	. . . . . . . . 9 ⊢ (Rel dom 𝑠 → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
22	20, 21	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
23	22	necon3bid 2988	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅))
24	17, 23	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ≠ ∅)
25		frxp3.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 Fr 𝐴)
26		df-fr 5544	. . . . . . . . 9 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑔((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎))
27	25, 26	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ∀𝑔((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎))
28	27	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∀𝑔((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎))
29		vex 3436	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
30	29	dmex 7758	. . . . . . . . 9 ⊢ dom 𝑠 ∈ V
31	30	dmex 7758	. . . . . . . 8 ⊢ dom dom 𝑠 ∈ V
32		sseq1 3946	. . . . . . . . . 10 ⊢ (𝑔 = dom dom 𝑠 → (𝑔 ⊆ 𝐴 ↔ dom dom 𝑠 ⊆ 𝐴))
33		neeq1 3006	. . . . . . . . . 10 ⊢ (𝑔 = dom dom 𝑠 → (𝑔 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅))
34	32, 33	anbi12d 631	. . . . . . . . 9 ⊢ (𝑔 = dom dom 𝑠 → ((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) ↔ (dom dom 𝑠 ⊆ 𝐴 ∧ dom dom 𝑠 ≠ ∅)))
35		raleq 3342	. . . . . . . . . 10 ⊢ (𝑔 = dom dom 𝑠 → (∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎 ↔ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎))
36	35	rexeqbi1dv 3341	. . . . . . . . 9 ⊢ (𝑔 = dom dom 𝑠 → (∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎 ↔ ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎))
37	34, 36	imbi12d 345	. . . . . . . 8 ⊢ (𝑔 = dom dom 𝑠 → (((𝑔 ⊆ 𝐴 ∧ 𝑔 ≠ ∅) → ∃𝑎 ∈ 𝑔 ∀𝑑 ∈ 𝑔 ¬ 𝑑𝑅𝑎) ↔ ((dom dom 𝑠 ⊆ 𝐴 ∧ dom dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)))
38	31, 37	spcv 3544	. . . . . . 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 696	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
41		imassrn 5980	. . . . . . . 8 ⊢ (dom 𝑠 “ {𝑎}) ⊆ ran dom 𝑠
42		rnss 5848	. . . . . . . . . . 11 ⊢ (dom 𝑠 ⊆ (𝐴 × 𝐵) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
43	4, 42	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
44		rnxpss 6075	. . . . . . . . . 10 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
45	43, 44	sstrdi 3933	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ 𝐵)
46	45	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ran dom 𝑠 ⊆ 𝐵)
47	41, 46	sstrid 3932	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ⊆ 𝐵)
48		simprl 768	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑎 ∈ dom dom 𝑠)
49		imadisj 5988	. . . . . . . . . 10 ⊢ ((dom 𝑠 “ {𝑎}) = ∅ ↔ (dom dom 𝑠 ∩ {𝑎}) = ∅)
50		disjsn 4647	. . . . . . . . . 10 ⊢ ((dom dom 𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠)
51	49, 50	bitri 274	. . . . . . . . 9 ⊢ ((dom 𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠)
52	51	necon2abii 2994	. . . . . . . 8 ⊢ (𝑎 ∈ dom dom 𝑠 ↔ (dom 𝑠 “ {𝑎}) ≠ ∅)
53	48, 52	sylib 217	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ≠ ∅)
54		frxp3.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 Fr 𝐵)
55		df-fr 5544	. . . . . . . . . 10 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑔((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏))
56	54, 55	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑔((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏))
57	30	imaex 7763	. . . . . . . . . 10 ⊢ (dom 𝑠 “ {𝑎}) ∈ V
58		sseq1 3946	. . . . . . . . . . . 12 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (𝑔 ⊆ 𝐵 ↔ (dom 𝑠 “ {𝑎}) ⊆ 𝐵))
59		neeq1 3006	. . . . . . . . . . . 12 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (𝑔 ≠ ∅ ↔ (dom 𝑠 “ {𝑎}) ≠ ∅))
60	58, 59	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → ((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) ↔ ((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅)))
61		raleq 3342	. . . . . . . . . . . 12 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏 ↔ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
62	61	rexeqbi1dv 3341	. . . . . . . . . . 11 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏 ↔ ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
63	60, 62	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑔 = (dom 𝑠 “ {𝑎}) → (((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏) ↔ (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)))
64	57, 63	spcv 3544	. . . . . . . . 9 ⊢ (∀𝑔((𝑔 ⊆ 𝐵 ∧ 𝑔 ≠ ∅) → ∃𝑏 ∈ 𝑔 ∀𝑒 ∈ 𝑔 ¬ 𝑒𝑆𝑏) → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
65	56, 64	syl 17	. . . . . . . 8 ⊢ (𝜑 → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
66	65	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (((dom 𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (dom 𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏))
67	47, 53, 66	mp2and 696	. . . . . 6 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
68		imassrn 5980	. . . . . . . . . 10 ⊢ (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ ran 𝑠
69		rnss 5848	. . . . . . . . . . . 12 ⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
70	69	ad2antrl 725	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
71		rnxpss 6075	. . . . . . . . . . 11 ⊢ ran ((𝐴 × 𝐵) × 𝐶) ⊆ 𝐶
72	70, 71	sstrdi 3933	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ 𝐶)
73	68, 72	sstrid 3932	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶)
74	73	ad2antrr 723	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶)
75		simprl 768	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 𝑏 ∈ (dom 𝑠 “ {𝑎}))
76		vex 3436	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
77		vex 3436	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
78	76, 77	elimasn 5997	. . . . . . . . . 10 ⊢ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
79	75, 78	sylib 217	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
80		imadisj 5988	. . . . . . . . . . 11 ⊢ ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ (dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅)
81		disjsn 4647	. . . . . . . . . . 11 ⊢ ((dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
82	80, 81	bitri 274	. . . . . . . . . 10 ⊢ ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
83	82	necon2abii 2994	. . . . . . . . 9 ⊢ (⟨𝑎, 𝑏⟩ ∈ dom 𝑠 ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
84	79, 83	sylib 217	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
85		frxp3.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 Fr 𝐶)
86		df-fr 5544	. . . . . . . . . . 11 ⊢ (𝑇 Fr 𝐶 ↔ ∀𝑔((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐))
87	85, 86	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑔((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐))
88	29	imaex 7763	. . . . . . . . . . 11 ⊢ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∈ V
89		sseq1 3946	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (𝑔 ⊆ 𝐶 ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶))
90		neeq1 3006	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (𝑔 ≠ ∅ ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅))
91	89, 90	anbi12d 631	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → ((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) ↔ ((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)))
92		raleq 3342	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐 ↔ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
93	92	rexeqbi1dv 3341	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐 ↔ ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
94	91, 93	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑠 “ {⟨𝑎, 𝑏⟩}) → (((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐) ↔ (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)))
95	88, 94	spcv 3544	. . . . . . . . . 10 ⊢ (∀𝑔((𝑔 ⊆ 𝐶 ∧ 𝑔 ≠ ∅) → ∃𝑐 ∈ 𝑔 ∀𝑓 ∈ 𝑔 ¬ 𝑓𝑇𝑐) → (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
96	87, 95	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
97	96	ad3antrrr 727	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (((𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶 ∧ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐))
98	74, 84, 97	mp2and 696	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
99		simprl 768	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → 𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}))
100		opex 5379	. . . . . . . . . 10 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
101		vex 3436	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
102	100, 101	elimasn 5997	. . . . . . . . 9 ⊢ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
103	99, 102	sylib 217	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
104		simplrl 774	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
105	104	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
106		elxpxpss 33684	. . . . . . . . . . 11 ⊢ ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ 𝑠) → ∃𝑔∃ℎ∃𝑖 𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩)
107	105, 106	sylan 580	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ∃𝑔∃ℎ∃𝑖 𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩)
108		df-ne 2944	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ≠ 𝑐 ↔ ¬ 𝑖 = 𝑐)
109	108	con2bii 358	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑐 ↔ ¬ 𝑖 ≠ 𝑐)
110	109	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑐 → ¬ 𝑖 ≠ 𝑐)
111	110	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ 𝑖 ≠ 𝑐)
112	111	intnand 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))
113		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑖 → (𝑓𝑇𝑐 ↔ 𝑖𝑇𝑐))
114	113	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑖 → (¬ 𝑓𝑇𝑐 ↔ ¬ 𝑖𝑇𝑐))
115		simplrr 775	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
116	115	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
117		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
118		vex 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑖 ∈ V
119	100, 118	elimasn 5997	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
120	117, 119	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}))
121	114, 116, 120	rspcdva 3562	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ 𝑖𝑇𝑐)
122		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐)
123	122	neneqd 2948	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ 𝑖 = 𝑐)
124		ioran 981	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐) ↔ (¬ 𝑖𝑇𝑐 ∧ ¬ 𝑖 = 𝑐))
125	121, 123, 124	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐))
126	125	intn3an3d 1480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)))
127	126	intnanrd 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))
128	112, 127	pm2.61dane 3032	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))
129		opeq2 4805	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = 𝑏 → ⟨𝑎, ℎ⟩ = ⟨𝑎, 𝑏⟩)
130	129	opeq1d 4810	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑏 → ⟨⟨𝑎, ℎ⟩, 𝑖⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑖⟩)
131	130	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑏 → (⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠 ↔ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠))
132	131	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)))
133		neeq1 3006	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = 𝑏 → (ℎ ≠ 𝑏 ↔ 𝑏 ≠ 𝑏))
134	133	orbi1d 914	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = 𝑏 → ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
135		neirr 2952	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ¬ 𝑏 ≠ 𝑏
136		orel1 886	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑏 ≠ 𝑏 → ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐))
137	135, 136	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐)
138		olc 865	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ≠ 𝑐 → (𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))
139	137, 138	impbii 208	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ 𝑖 ≠ 𝑐)
140	134, 139	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑏 → ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ 𝑖 ≠ 𝑐))
141	140	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑏 → ((((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)))
142	141	notbid 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑏 → (¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)))
143	132, 142	imbi12d 345	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ = 𝑏 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))))
144	128, 143	mpbiri 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
145	144	impcom 408	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ = 𝑏) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
146		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = ℎ → (𝑒𝑆𝑏 ↔ ℎ𝑆𝑏))
147	146	notbid 318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑒 = ℎ → (¬ 𝑒𝑆𝑏 ↔ ¬ ℎ𝑆𝑏))
148		simplrr 775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
149	148	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
150		opex 5379	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ⟨𝑎, ℎ⟩ ∈ V
151	150, 118	opeldm 5816	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑎, ℎ⟩ ∈ dom 𝑠)
152	151	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ⟨𝑎, ℎ⟩ ∈ dom 𝑠)
153	152	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ⟨𝑎, ℎ⟩ ∈ dom 𝑠)
154		vex 3436	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℎ ∈ V
155	76, 154	elimasn 5997	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, ℎ⟩ ∈ dom 𝑠)
156	153, 155	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ℎ ∈ (dom 𝑠 “ {𝑎}))
157	147, 149, 156	rspcdva 3562	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ℎ𝑆𝑏)
158		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ℎ ≠ 𝑏)
159	158	neneqd 2948	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ℎ = 𝑏)
160		ioran 981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ↔ (¬ ℎ𝑆𝑏 ∧ ¬ ℎ = 𝑏))
161	157, 159, 160	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ (ℎ𝑆𝑏 ∨ ℎ = 𝑏))
162	161	intn3an2d 1479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)))
163	162	intnanrd 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
164	145, 163	pm2.61dane 3032	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
165		opeq1 4804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = 𝑎 → ⟨𝑔, ℎ⟩ = ⟨𝑎, ℎ⟩)
166	165	opeq1d 4810	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑎 → ⟨⟨𝑔, ℎ⟩, 𝑖⟩ = ⟨⟨𝑎, ℎ⟩, 𝑖⟩)
167	166	eleq1d 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑎 → (⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠 ↔ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠))
168	167	anbi2d 629	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠)))
169		3orass 1089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑔 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
170		neeq1 3006	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 = 𝑎 → (𝑔 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
171	170	orbi1d 914	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
172	169, 171	syl5bb 283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
173		neirr 2952	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ 𝑎 ≠ 𝑎
174		orel1 886	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑎 ≠ 𝑎 → ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) → (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
175	173, 174	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) → (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))
176		olc 865	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
177	175, 176	impbii 208	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))
178	172, 177	bitrdi 287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
179	178	anbi2d 629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑎 → ((((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
180	179	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑎 → (¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
181	168, 180	imbi12d 345	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑎 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))))
182	164, 181	mpbiri 257	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
183	182	impcom 408	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 = 𝑎) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
184		breq1 5077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑔 → (𝑑𝑅𝑎 ↔ 𝑔𝑅𝑎))
185	184	notbid 318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑔 → (¬ 𝑑𝑅𝑎 ↔ ¬ 𝑔𝑅𝑎))
186		simplrr 775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
187	186	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
188		opex 5379	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ⟨𝑔, ℎ⟩ ∈ V
189	188, 118	opeldm 5816	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑔, ℎ⟩ ∈ dom 𝑠)
190	189	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ⟨𝑔, ℎ⟩ ∈ dom 𝑠)
191		vex 3436	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑔 ∈ V
192	191, 154	opeldm 5816	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑔, ℎ⟩ ∈ dom 𝑠 → 𝑔 ∈ dom dom 𝑠)
193	190, 192	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → 𝑔 ∈ dom dom 𝑠)
194	193	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 𝑔 ∈ dom dom 𝑠)
195	185, 187, 194	rspcdva 3562	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ 𝑔𝑅𝑎)
196		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 𝑔 ≠ 𝑎)
197	196	neneqd 2948	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ 𝑔 = 𝑎)
198		ioran 981	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ↔ (¬ 𝑔𝑅𝑎 ∧ ¬ 𝑔 = 𝑎))
199	195, 197, 198	sylanbrc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ (𝑔𝑅𝑎 ∨ 𝑔 = 𝑎))
200	199	intn3an1d 1478	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)))
201	200	intnanrd 490	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
202	183, 201	pm2.61dane 3032	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
203	202	intn3an3d 1480	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
204		eleq1 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → (𝑞 ∈ 𝑠 ↔ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠))
205	204	anbi2d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠)))
206		breq1 5077	. . . . . . . . . . . . . . . . 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 33795	. . . . . . . . . . . . . . . . 17 ⊢ (⟨⟨𝑔, ℎ⟩, 𝑖⟩𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
209	206, 208	bitrdi 287	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))))
210	209	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → (¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))))
211	205, 210	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))))
212	203, 211	mpbiri 257	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
213	212	com12 32	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
214	213	exlimdv 1936	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑖 𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
215	214	exlimdvv 1937	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑔∃ℎ∃𝑖 𝑞 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
216	107, 215	mpd 15	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩)
217	216	ralrimiva 3103	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩)
218		breq2 5078	. . . . . . . . . . 11 ⊢ (𝑝 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (𝑞𝑈𝑝 ↔ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
219	218	notbid 318	. . . . . . . . . 10 ⊢ (𝑝 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (¬ 𝑞𝑈𝑝 ↔ ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
220	219	ralbidv 3112	. . . . . . . . 9 ⊢ (𝑝 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝 ↔ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
221	220	rspcev 3561	. . . . . . . 8 ⊢ ((⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠 ∧ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
222	103, 217, 221	syl2anc 584	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
223	98, 222	rexlimddv 3220	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
224	67, 223	rexlimddv 3220	. . . . 5 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
225	40, 224	rexlimddv 3220	. . . 4 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
226	225	ex 413	. . 3 ⊢ (𝜑 → ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝))
227	226	alrimiv 1930	. 2 ⊢ (𝜑 → ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝))
228		df-fr 5544	. 2 ⊢ (𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ↔ ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝))
229	227, 228	sylibr 233	1 ⊢ (𝜑 → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∨ w3o 1085 ∧ w3a 1086 ∀wal 1537 = wceq 1539 ∃wex 1782 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 ∩ cin 3886 ⊆ wss 3887 ∅c0 4256 {csn 4561 ⟨cop 4567 class class class wbr 5074 {copab 5136 Fr wfr 5541 × cxp 5587 dom cdm 5589 ran crn 5590 “ cima 5592 Rel wrel 5594 ‘cfv 6433 1^st c1st 7829 2^nd c2nd 7830

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 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 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-fr 5544 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-iota 6391 df-fun 6435 df-fv 6441 df-1st 7831 df-2nd 7832

This theorem is referenced by: xpord3ind 33800

W3C validator