Theorem dfpo2 6305

Description: Quantifier-free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)

Assertion

Ref	Expression
dfpo2	⊢ (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))

Proof of Theorem dfpo2

Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		po0 5579	. . . 4 ⊢ 𝑅 Po ∅
2		res0 5978	. . . . . . 7 ⊢ ( I ↾ ∅) = ∅
3	2	ineq2i 4116	. . . . . 6 ⊢ (𝑅 ∩ ( I ↾ ∅)) = (𝑅 ∩ ∅)
4		in0 4347	. . . . . 6 ⊢ (𝑅 ∩ ∅) = ∅
5	3, 4	eqtri 2786	. . . . 5 ⊢ (𝑅 ∩ ( I ↾ ∅)) = ∅
6		xp0 5755	. . . . . . . . . 10 ⊢ (𝐴 × ∅) = ∅
7	6	ineq2i 4116	. . . . . . . . 9 ⊢ (𝑅 ∩ (𝐴 × ∅)) = (𝑅 ∩ ∅)
8	7, 4	eqtri 2786	. . . . . . . 8 ⊢ (𝑅 ∩ (𝐴 × ∅)) = ∅
9	8	coeq2i 5842	. . . . . . 7 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅)
10		co02 6268	. . . . . . 7 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅) = ∅
11	9, 10	eqtri 2786	. . . . . 6 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ∅
12		0ss 4352	. . . . . 6 ⊢ ∅ ⊆ 𝑅
13	11, 12	eqsstri 3958	. . . . 5 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅
14	5, 13	pm3.2i 476	. . . 4 ⊢ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)
15	1, 14	2th 267	. . 3 ⊢ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
16		poeq2 5566	. . . 4 ⊢ (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ 𝑅 Po ∅))
17		reseq2 5969	. . . . . . 7 ⊢ (𝐴 = ∅ → ( I ↾ 𝐴) = ( I ↾ ∅))
18	17	ineq2d 4119	. . . . . 6 ⊢ (𝐴 = ∅ → (𝑅 ∩ ( I ↾ 𝐴)) = (𝑅 ∩ ( I ↾ ∅)))
19	18	eqeq1d 2765	. . . . 5 ⊢ (𝐴 = ∅ → ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ (𝑅 ∩ ( I ↾ ∅)) = ∅))
20		xpeq2 5675	. . . . . . . 8 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (𝐴 × ∅))
21	20	ineq2d 4119	. . . . . . 7 ⊢ (𝐴 = ∅ → (𝑅 ∩ (𝐴 × 𝐴)) = (𝑅 ∩ (𝐴 × ∅)))
22	21	coeq2d 5844	. . . . . 6 ⊢ (𝐴 = ∅ → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))))
23	22	sseq1d 3943	. . . . 5 ⊢ (𝐴 = ∅ → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
24	19, 23	anbi12d 644	. . . 4 ⊢ (𝐴 = ∅ → (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)))
25	16, 24	bibi12d 348	. . 3 ⊢ (𝐴 = ∅ → ((𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) ↔ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))))
26	15, 25	mpbiri 261	. 2 ⊢ (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
27		r19.28zv 4464	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → (∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
28	27	ralbidv 3188	. . . . . 6 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
29		r19.28zv 4464	. . . . . 6 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
30	28, 29	bitrd 282	. . . . 5 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
31	30	ralbidv 3188	. . . 4 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
32		r19.26 3125	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
33	31, 32	bitrdi 290	. . 3 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
34		df-po 5562	. . 3 ⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
35		disj 4405	. . . . 5 ⊢ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑤 ∈ 𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴))
36		df-ral 3080	. . . . 5 ⊢ (∀𝑤 ∈ 𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
37		opex 5435	. . . . . . . . . 10 ⊢ ⟨𝑥, 𝑥⟩ ∈ V
38		eleq1 2851	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ 𝑅 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅))
39		df-br 5106	. . . . . . . . . . . 12 ⊢ (𝑥𝑅𝑥 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅)
40	38, 39	bitr4di 292	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ 𝑅 ↔ 𝑥𝑅𝑥))
41		eleq1 2851	. . . . . . . . . . . . 13 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴)))
42		opelidres 5986	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ V → (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥 ∈ 𝐴))
43	42	elv 3458	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥 ∈ 𝐴)
44	41, 43	bitrdi 290	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ 𝑥 ∈ 𝐴))
45	44	notbid 321	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴))
46	40, 45	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → ((𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ (𝑥𝑅𝑥 → ¬ 𝑥 ∈ 𝐴)))
47	37, 46	spcv 3562	. . . . . . . . 9 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝑅𝑥 → ¬ 𝑥 ∈ 𝐴))
48	47	con2d 135	. . . . . . . 8 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
49	48	alrimiv 1961	. . . . . . 7 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
50		relres 6000	. . . . . . . . . . . 12 ⊢ Rel ( I ↾ 𝐴)
51		elrel 5778	. . . . . . . . . . . 12 ⊢ ((Rel ( I ↾ 𝐴) ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
52	50, 51	mpan 703	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ( I ↾ 𝐴) → ∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
53	52	ancri 559	. . . . . . . . . 10 ⊢ (𝑤 ∈ ( I ↾ 𝐴) → (∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)))
54		eleq1 2851	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
55		breq12 5110	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥𝑅𝑥 ↔ 𝑦𝑅𝑦))
56	55	anidms 577	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑥𝑅𝑥 ↔ 𝑦𝑅𝑦))
57	56	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑦𝑅𝑦))
58	54, 57	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) ↔ (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦)))
59	58	spvv 2022	. . . . . . . . . . . . . 14 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦))
60		breq2 5109	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑦 ↔ 𝑦𝑅𝑧))
61	60	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → (¬ 𝑦𝑅𝑦 ↔ ¬ 𝑦𝑅𝑧))
62	61	imbi2d 343	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) ↔ (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑧)))
63	62	biimpcd 252	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) → (𝑦 = 𝑧 → (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑧)))
64	63	impcomd 417	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) → ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
65	59, 64	syl 18	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
66		eleq1 2851	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴)))
67		vex 3457	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
68	67	brresi 5983	. . . . . . . . . . . . . . . 16 ⊢ (𝑦( I ↾ 𝐴)𝑧 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 I 𝑧))
69		df-br 5106	. . . . . . . . . . . . . . . 16 ⊢ (𝑦( I ↾ 𝐴)𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
70	67	ideq 5834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 I 𝑧 ↔ 𝑦 = 𝑧)
71	70	anbi2i 635	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 I 𝑧) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧))
72	68, 69, 71	3bitr3ri 305	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
73	66, 72	bitr4di 292	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧)))
74		eleq1 2851	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ 𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
75		df-br 5106	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑅𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅)
76	74, 75	bitr4di 292	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ 𝑅 ↔ 𝑦𝑅𝑧))
77	76	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (¬ 𝑤 ∈ 𝑅 ↔ ¬ 𝑦𝑅𝑧))
78	73, 77	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧)))
79	65, 78	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅)))
80	79	exlimdvv 1968	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅)))
81	80	impd 416	. . . . . . . . . 10 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ((∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ¬ 𝑤 ∈ 𝑅))
82	53, 81	syl5 35	. . . . . . . . 9 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅))
83	82	con2d 135	. . . . . . . 8 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
84	83	alrimiv 1961	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
85	49, 84	impbii 212	. . . . . 6 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
86		df-ral 3080	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
87	85, 86	bitr4i 281	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥)
88	35, 36, 87	3bitri 300	. . . 4 ⊢ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥)
89		ralcom 3293	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
90		r19.23v 3192	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
91	90	ralbii 3111	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
92	89, 91	bitri 278	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
93	92	ralbii 3111	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
94		brin 5159	. . . . . . . . . . . 12 ⊢ (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ↔ (𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦))
95		brin 5159	. . . . . . . . . . . 12 ⊢ (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧 ↔ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧))
96	94, 95	anbi12i 640	. . . . . . . . . . 11 ⊢ ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)))
97		an4 669	. . . . . . . . . . . 12 ⊢ (((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧)))
98		ancom 466	. . . . . . . . . . . 12 ⊢ (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
99		ancom 466	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴))
100	99	anbi1i 636	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
101		brxp 5703	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝐴 × 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴))
102		brxp 5703	. . . . . . . . . . . . . . 15 ⊢ (𝑦(𝐴 × 𝐴)𝑧 ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))
103	101, 102	anbi12i 640	. . . . . . . . . . . . . 14 ⊢ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
104		anandi 689	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
105	100, 103, 104	3bitr4i 306	. . . . . . . . . . . . 13 ⊢ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ↔ (𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
106	105	anbi1i 636	. . . . . . . . . . . 12 ⊢ (((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
107	97, 98, 106	3bitri 300	. . . . . . . . . . 11 ⊢ (((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
108		anass 474	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ (𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
109	96, 107, 108	3bitri 300	. . . . . . . . . 10 ⊢ ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ (𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
110	109	exbii 1880	. . . . . . . . 9 ⊢ (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
111		vex 3457	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
112	111, 67	brco 5852	. . . . . . . . . 10 ⊢ (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧))
113		df-br 5106	. . . . . . . . . 10 ⊢ (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
114	112, 113	bitr3i 280	. . . . . . . . 9 ⊢ (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
115		df-rex 3090	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
116		r19.42v 3197	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
117	115, 116	bitr3i 280	. . . . . . . . 9 ⊢ (∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
118	110, 114, 117	3bitr3ri 305	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
119		df-br 5106	. . . . . . . 8 ⊢ (𝑥𝑅𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑅)
120	118, 119	imbi12i 353	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ (⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
121	120	2albii 1852	. . . . . 6 ⊢ (∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
122		r2al 3201	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
123		impexp 456	. . . . . . . 8 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
124	123	2albii 1852	. . . . . . 7 ⊢ (∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
125	122, 124	bitr4i 281	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
126		relco 6109	. . . . . . 7 ⊢ Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))
127		ssrel 5763	. . . . . . 7 ⊢ (Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅)))
128	126, 127	ax-mp 5	. . . . . 6 ⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
129	121, 125, 128	3bitr4i 306	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)
130	93, 129	bitr2i 279	. . . 4 ⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
131	88, 130	anbi12i 640	. . 3 ⊢ (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
132	33, 34, 131	3bitr4g 317	. 2 ⊢ (𝐴 ≠ ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
133	26, 132	pm2.61ine 3041	1 ⊢ (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2146   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  Vcvv 3453   ⊆ wss 3899   ∩ cin 4091  ∅c0 4280  ⟨cop 4837   class class class wbr 5105   I cid 5548   Po wpo 5560   × cxp 5652   ↾ cres 5656   ∘ ccom 5658  Rel wrel 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106  df-opab 5170  df-id 5549  df-po 5562  df-xp 5660  df-rel 5661  df-co 5663  df-res 5666

This theorem is used by:  predpo  6332