frxp3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > frxp3		Structured version Visualization version GIF version

Theorem frxp3 8155

Description: Give well-foundedness over a triple Cartesian 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		frxp3.1	. . . . . . 7 ⊢ (𝜑 → 𝑅 Fr 𝐴)
2	1	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → 𝑅 Fr 𝐴)
3		dmss 5887	. . . . . . . . . 10 ⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
4	3	ad2antrl 728	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶))
5		dmxpss 6165	. . . . . . . . 9 ⊢ dom ((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵)
6	4, 5	sstrdi 3976	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom 𝑠 ⊆ (𝐴 × 𝐵))
7		dmss 5887	. . . . . . . 8 ⊢ (dom 𝑠 ⊆ (𝐴 × 𝐵) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
8	6, 7	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ dom (𝐴 × 𝐵))
9		dmxpss 6165	. . . . . . 7 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
10	8, 9	sstrdi 3976	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ⊆ 𝐴)
11		vex 3468	. . . . . . . . 9 ⊢ 𝑠 ∈ V
12	11	dmex 7910	. . . . . . . 8 ⊢ dom 𝑠 ∈ V
13	12	dmex 7910	. . . . . . 7 ⊢ dom dom 𝑠 ∈ V
14	13	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ∈ V)
15		relxp 5677	. . . . . . . . . . . . 13 ⊢ Rel ((𝐴 × 𝐵) × 𝐶)
16		relss 5765	. . . . . . . . . . . . 13 ⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → (Rel ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠))
17	15, 16	mpi 20	. . . . . . . . . . . 12 ⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → Rel 𝑠)
18	17	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → Rel 𝑠)
19		reldm0 5912	. . . . . . . . . . 11 ⊢ (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
20	18, 19	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
21		relxp 5677	. . . . . . . . . . . . . 14 ⊢ Rel (𝐴 × 𝐵)
22		relss 5765	. . . . . . . . . . . . . 14 ⊢ (dom ((𝐴 × 𝐵) × 𝐶) ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel dom ((𝐴 × 𝐵) × 𝐶)))
23	5, 21, 22	mp2 9	. . . . . . . . . . . . 13 ⊢ Rel dom ((𝐴 × 𝐵) × 𝐶)
24		relss 5765	. . . . . . . . . . . . 13 ⊢ (dom 𝑠 ⊆ dom ((𝐴 × 𝐵) × 𝐶) → (Rel dom ((𝐴 × 𝐵) × 𝐶) → Rel dom 𝑠))
25	3, 23, 24	mpisyl 21	. . . . . . . . . . . 12 ⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → Rel dom 𝑠)
26	25	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → Rel dom 𝑠)
27		reldm0 5912	. . . . . . . . . . 11 ⊢ (Rel dom 𝑠 → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
28	26, 27	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
29	20, 28	bitrd 279	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 = ∅ ↔ dom dom 𝑠 = ∅))
30	29	necon3bid 2977	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → (𝑠 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅))
31	30	biimpa 476	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) ∧ 𝑠 ≠ ∅) → dom dom 𝑠 ≠ ∅)
32	31	anasss 466	. . . . . 6 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → dom dom 𝑠 ≠ ∅)
33	2, 10, 14, 32	frd 5615	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑎 ∈ dom dom 𝑠∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
34		frxp3.2	. . . . . . . 8 ⊢ (𝜑 → 𝑆 Fr 𝐵)
35	34	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑆 Fr 𝐵)
36		imassrn 6063	. . . . . . . . 9 ⊢ (dom 𝑠 “ {𝑎}) ⊆ ran dom 𝑠
37		rnss 5924	. . . . . . . . . . 11 ⊢ (dom 𝑠 ⊆ (𝐴 × 𝐵) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
38	6, 37	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ ran (𝐴 × 𝐵))
39		rnxpss 6166	. . . . . . . . . 10 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
40	38, 39	sstrdi 3976	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran dom 𝑠 ⊆ 𝐵)
41	36, 40	sstrid 3975	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (dom 𝑠 “ {𝑎}) ⊆ 𝐵)
42	41	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ⊆ 𝐵)
43	12	imaex 7915	. . . . . . . 8 ⊢ (dom 𝑠 “ {𝑎}) ∈ V
44	43	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ∈ V)
45		imadisj 6072	. . . . . . . . . . 11 ⊢ ((dom 𝑠 “ {𝑎}) = ∅ ↔ (dom dom 𝑠 ∩ {𝑎}) = ∅)
46		disjsn 4692	. . . . . . . . . . 11 ⊢ ((dom dom 𝑠 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠)
47	45, 46	bitri 275	. . . . . . . . . 10 ⊢ ((dom 𝑠 “ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠)
48	47	necon2abii 2983	. . . . . . . . 9 ⊢ (𝑎 ∈ dom dom 𝑠 ↔ (dom 𝑠 “ {𝑎}) ≠ ∅)
49	48	biimpi 216	. . . . . . . 8 ⊢ (𝑎 ∈ dom dom 𝑠 → (dom 𝑠 “ {𝑎}) ≠ ∅)
50	49	ad2antrl 728	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → (dom 𝑠 “ {𝑎}) ≠ ∅)
51	35, 42, 44, 50	frd 5615	. . . . . 6 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑏 ∈ (dom 𝑠 “ {𝑎})∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
52		frxp3.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 Fr 𝐶)
53	52	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 𝑇 Fr 𝐶)
54		imassrn 6063	. . . . . . . . . 10 ⊢ (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ ran 𝑠
55		rnss 5924	. . . . . . . . . . . 12 ⊢ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
56	55	ad2antrl 728	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ ran ((𝐴 × 𝐵) × 𝐶))
57		rnxpss 6166	. . . . . . . . . . 11 ⊢ ran ((𝐴 × 𝐵) × 𝐶) ⊆ 𝐶
58	56, 57	sstrdi 3976	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ran 𝑠 ⊆ 𝐶)
59	54, 58	sstrid 3975	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶)
60	59	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ⊆ 𝐶)
61	11	imaex 7915	. . . . . . . . 9 ⊢ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∈ V
62	61	a1i 11	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ∈ V)
63		simprl 770	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → 𝑏 ∈ (dom 𝑠 “ {𝑎}))
64		vex 3468	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
65		vex 3468	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
66	64, 65	elimasn 6082	. . . . . . . . . 10 ⊢ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
67	63, 66	sylib 218	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
68		imadisj 6072	. . . . . . . . . . 11 ⊢ ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ (dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅)
69		disjsn 4692	. . . . . . . . . . 11 ⊢ ((dom 𝑠 ∩ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
70	68, 69	bitri 275	. . . . . . . . . 10 ⊢ ((𝑠 “ {⟨𝑎, 𝑏⟩}) = ∅ ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ dom 𝑠)
71	70	necon2abii 2983	. . . . . . . . 9 ⊢ (⟨𝑎, 𝑏⟩ ∈ dom 𝑠 ↔ (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
72	67, 71	sylib 218	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → (𝑠 “ {⟨𝑎, 𝑏⟩}) ≠ ∅)
73	53, 60, 62, 72	frd 5615	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩})∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
74		df-ot 4615	. . . . . . . . 9 ⊢ ⟨𝑎, 𝑏, 𝑐⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩
75		simprl 770	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → 𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}))
76		opex 5444	. . . . . . . . . . 11 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
77		vex 3468	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
78	76, 77	elimasn 6082	. . . . . . . . . 10 ⊢ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
79	75, 78	sylib 218	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ 𝑠)
80	74, 79	eqeltrid 2839	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ⟨𝑎, 𝑏, 𝑐⟩ ∈ 𝑠)
81		simplrl 776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
82	81	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶))
83		el2xpss 8041	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ 𝑠 ∧ 𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶)) → ∃𝑔∃ℎ∃𝑖 𝑞 = ⟨𝑔, ℎ, 𝑖⟩)
84	83	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ 𝑠) → ∃𝑔∃ℎ∃𝑖 𝑞 = ⟨𝑔, ℎ, 𝑖⟩)
85	82, 84	sylan 580	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ∃𝑔∃ℎ∃𝑖 𝑞 = ⟨𝑔, ℎ, 𝑖⟩)
86		df-ne 2934	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ≠ 𝑐 ↔ ¬ 𝑖 = 𝑐)
87	86	con2bii 357	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑐 ↔ ¬ 𝑖 ≠ 𝑐)
88	87	biimpi 216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑐 → ¬ 𝑖 ≠ 𝑐)
89	88	intnand 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑐 → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))
90	89	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 = 𝑐) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))
91		breq1 5127	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑖 → (𝑓𝑇𝑐 ↔ 𝑖𝑇𝑐))
92	91	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑖 → (¬ 𝑓𝑇𝑐 ↔ ¬ 𝑖𝑇𝑐))
93		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
94	93	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)
95		df-ot 4615	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ⟨𝑎, 𝑏, 𝑖⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑖⟩
96		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠)
97	95, 96	eqeltrrid 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
98		vex 3468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑖 ∈ V
99	76, 98	elimasn 6082	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑖⟩ ∈ 𝑠)
100	97, 99	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 𝑖 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}))
101	92, 94, 100	rspcdva 3607	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ 𝑖𝑇𝑐)
102		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐)
103	102	neneqd 2938	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ 𝑖 = 𝑐)
104		ioran 985	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐) ↔ (¬ 𝑖𝑇𝑐 ∧ ¬ 𝑖 = 𝑐))
105	101, 103, 104	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐))
106	105	intn3an3d 1483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)))
107	106	intnanrd 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) ∧ 𝑖 ≠ 𝑐) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))
108	90, 107	pm2.61dane 3020	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))
109		oteq2 4864	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑏 → ⟨𝑎, ℎ, 𝑖⟩ = ⟨𝑎, 𝑏, 𝑖⟩)
110	109	eleq1d 2820	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑏 → (⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠))
111	110	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠)))
112		neeq1 2995	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = 𝑏 → (ℎ ≠ 𝑏 ↔ 𝑏 ≠ 𝑏))
113	112	orbi1d 916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = 𝑏 → ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
114		neirr 2942	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ¬ 𝑏 ≠ 𝑏
115		orel1 888	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑏 ≠ 𝑏 → ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐))
116	114, 115	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → 𝑖 ≠ 𝑐)
117		olc 868	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ≠ 𝑐 → (𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))
118	116, 117	impbii 209	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ 𝑖 ≠ 𝑐)
119	113, 118	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑏 → ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ 𝑖 ≠ 𝑐))
120	119	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑏 → ((((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)))
121	120	notbid 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑏 → (¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐)))
122	111, 121	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ = 𝑏 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, 𝑏, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ 𝑖 ≠ 𝑐))))
123	108, 122	mpbiri 258	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑏 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
124	123	impcom 407	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ = 𝑏) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
125		breq1 5127	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = ℎ → (𝑒𝑆𝑏 ↔ ℎ𝑆𝑏))
126	125	notbid 318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑒 = ℎ → (¬ 𝑒𝑆𝑏 ↔ ¬ ℎ𝑆𝑏))
127		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
128	127	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)
129		df-ot 4615	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⟨𝑎, ℎ, 𝑖⟩ = ⟨⟨𝑎, ℎ⟩, 𝑖⟩
130		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠)
131	129, 130	eqeltrrid 2840	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠)
132		opex 5444	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⟨𝑎, ℎ⟩ ∈ V
133	132, 98	opeldm 5892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨⟨𝑎, ℎ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑎, ℎ⟩ ∈ dom 𝑠)
134	131, 133	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ⟨𝑎, ℎ⟩ ∈ dom 𝑠)
135		vex 3468	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℎ ∈ V
136	64, 135	elimasn 6082	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ∈ (dom 𝑠 “ {𝑎}) ↔ ⟨𝑎, ℎ⟩ ∈ dom 𝑠)
137	134, 136	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ℎ ∈ (dom 𝑠 “ {𝑎}))
138	126, 128, 137	rspcdva 3607	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ℎ𝑆𝑏)
139		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ℎ ≠ 𝑏)
140	139	neneqd 2938	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ℎ = 𝑏)
141		ioran 985	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ↔ (¬ ℎ𝑆𝑏 ∧ ¬ ℎ = 𝑏))
142	138, 140, 141	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ (ℎ𝑆𝑏 ∨ ℎ = 𝑏))
143	142	intn3an2d 1482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)))
144	143	intnanrd 489	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) ∧ ℎ ≠ 𝑏) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
145	124, 144	pm2.61dane 3020	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
146		oteq1 4863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑎 → ⟨𝑔, ℎ, 𝑖⟩ = ⟨𝑎, ℎ, 𝑖⟩)
147	146	eleq1d 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑎 → (⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠 ↔ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠))
148	147	anbi2d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠)))
149		neeq1 2995	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = 𝑎 → (𝑔 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
150		biidd 262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = 𝑎 → (ℎ ≠ 𝑏 ↔ ℎ ≠ 𝑏))
151		biidd 262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = 𝑎 → (𝑖 ≠ 𝑐 ↔ 𝑖 ≠ 𝑐))
152	149, 150, 151	3orbi123d 1437	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
153		3orass 1089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
154		neirr 2942	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ¬ 𝑎 ≠ 𝑎
155		orel1 888	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑎 ≠ 𝑎 → ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) → (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
156	154, 155	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) → (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))
157		olc 868	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) → (𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
158	156, 157	impbii 209	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ≠ 𝑎 ∨ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))
159	153, 158	bitri 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))
160	152, 159	bitrdi 287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑎 → ((𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐) ↔ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
161	160	anbi2d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑎 → ((((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
162	161	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑎 → (¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)) ↔ ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
163	148, 162	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑎 → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑎, ℎ, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))))
164	145, 163	mpbiri 258	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
165	164	impcom 407	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 = 𝑎) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
166		breq1 5127	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑔 → (𝑑𝑅𝑎 ↔ 𝑔𝑅𝑎))
167	166	notbid 318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑔 → (¬ 𝑑𝑅𝑎 ↔ ¬ 𝑔𝑅𝑎))
168		simplrr 777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
169	168	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)
170		df-ot 4615	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⟨𝑔, ℎ, 𝑖⟩ = ⟨⟨𝑔, ℎ⟩, 𝑖⟩
171		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠)
172	170, 171	eqeltrrid 2840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠)
173		opex 5444	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⟨𝑔, ℎ⟩ ∈ V
174	173, 98	opeldm 5892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∈ 𝑠 → ⟨𝑔, ℎ⟩ ∈ dom 𝑠)
175		vex 3468	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑔 ∈ V
176	175, 135	opeldm 5892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑔, ℎ⟩ ∈ dom 𝑠 → 𝑔 ∈ dom dom 𝑠)
177	172, 174, 176	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 𝑔 ∈ dom dom 𝑠)
178	167, 169, 177	rspcdva 3607	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ 𝑔𝑅𝑎)
179		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → 𝑔 ≠ 𝑎)
180	179	neneqd 2938	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ 𝑔 = 𝑎)
181		ioran 985	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ↔ (¬ 𝑔𝑅𝑎 ∧ ¬ 𝑔 = 𝑎))
182	178, 180, 181	sylanbrc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ (𝑔𝑅𝑎 ∨ 𝑔 = 𝑎))
183	182	intn3an1d 1481	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ ((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)))
184	183	intnanrd 489	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) ∧ 𝑔 ≠ 𝑎) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
185	165, 184	pm2.61dane 3020	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) → ¬ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))
186	185	intn3an3d 1483	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
187		eleq1 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = ⟨𝑔, ℎ, 𝑖⟩ → (𝑞 ∈ 𝑠 ↔ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠))
188	187	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ⟨𝑔, ℎ, 𝑖⟩ → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) ↔ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠)))
189		breq1 5127	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑔, ℎ, 𝑖⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ⟨𝑔, ℎ, 𝑖⟩𝑈⟨𝑎, 𝑏, 𝑐⟩))
190		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 ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
191	190	xpord3lem 8153	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑔, ℎ, 𝑖⟩𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))
192	189, 191	bitrdi 287	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = ⟨𝑔, ℎ, 𝑖⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))))
193	192	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ⟨𝑔, ℎ, 𝑖⟩ → (¬ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐)))))
194	188, 193	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ⟨𝑔, ℎ, 𝑖⟩ → (((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩) ↔ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ ⟨𝑔, ℎ, 𝑖⟩ ∈ 𝑠) → ¬ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑔𝑅𝑎 ∨ 𝑔 = 𝑎) ∧ (ℎ𝑆𝑏 ∨ ℎ = 𝑏) ∧ (𝑖𝑇𝑐 ∨ 𝑖 = 𝑐)) ∧ (𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐))))))
195	186, 194	mpbiri 258	. . . . . . . . . . . . 13 ⊢ (𝑞 = ⟨𝑔, ℎ, 𝑖⟩ → ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩))
196	195	com12 32	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (𝑞 = ⟨𝑔, ℎ, 𝑖⟩ → ¬ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩))
197	196	exlimdv 1933	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑖 𝑞 = ⟨𝑔, ℎ, 𝑖⟩ → ¬ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩))
198	197	exlimdvv 1934	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → (∃𝑔∃ℎ∃𝑖 𝑞 = ⟨𝑔, ℎ, 𝑖⟩ → ¬ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩))
199	85, 198	mpd 15	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) ∧ 𝑞 ∈ 𝑠) → ¬ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩)
200	199	ralrimiva 3133	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩)
201		breq2 5128	. . . . . . . . . . 11 ⊢ (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑞𝑈𝑝 ↔ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩))
202	201	notbid 318	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → (¬ 𝑞𝑈𝑝 ↔ ¬ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩))
203	202	ralbidv 3164	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → (∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝 ↔ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩))
204	203	rspcev 3606	. . . . . . . 8 ⊢ ((⟨𝑎, 𝑏, 𝑐⟩ ∈ 𝑠 ∧ ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
205	80, 200, 204	syl2anc 584	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) ∧ (𝑐 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ∧ ∀𝑓 ∈ (𝑠 “ {⟨𝑎, 𝑏⟩}) ¬ 𝑓𝑇𝑐)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
206	73, 205	rexlimddv 3148	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) ∧ (𝑏 ∈ (dom 𝑠 “ {𝑎}) ∧ ∀𝑒 ∈ (dom 𝑠 “ {𝑎}) ¬ 𝑒𝑆𝑏)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
207	51, 206	rexlimddv 3148	. . . . 5 ⊢ (((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) ∧ (𝑎 ∈ dom dom 𝑠 ∧ ∀𝑑 ∈ dom dom 𝑠 ¬ 𝑑𝑅𝑎)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
208	33, 207	rexlimddv 3148	. . . 4 ⊢ ((𝜑 ∧ (𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅)) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝)
209	208	ex 412	. . 3 ⊢ (𝜑 → ((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝))
210	209	alrimiv 1927	. 2 ⊢ (𝜑 → ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝))
211		df-fr 5611	. 2 ⊢ (𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ↔ ∀𝑠((𝑠 ⊆ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑠 ≠ ∅) → ∃𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ¬ 𝑞𝑈𝑝))
212	210, 211	sylibr 234	1 ⊢ (𝜑 → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∨ w3o 1085 ∧ w3a 1086 ∀wal 1538 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 Vcvv 3464 ∩ cin 3930 ⊆ wss 3931 ∅c0 4313 {csn 4606 ⟨cop 4612 ⟨cotp 4614 class class class wbr 5124 {copab 5186 Fr wfr 5608 × cxp 5657 dom cdm 5659 ran crn 5660 “ cima 5662 Rel wrel 5664 ‘cfv 6536 1^st c1st 7991 2^nd c2nd 7992

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pr 5407 ax-un 7734

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-ot 4615 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-id 5553 df-fr 5611 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6489 df-fun 6538 df-fv 6544 df-1st 7993 df-2nd 7994

This theorem is referenced by: xpord3inddlem 8158

W3C validator