Theorem dfpo2 6199

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 5520	. . . 4 ⊢ 𝑅 Po ∅
2		res0 5895	. . . . . . 7 ⊢ ( I ↾ ∅) = ∅
3	2	ineq2i 4143	. . . . . 6 ⊢ (𝑅 ∩ ( I ↾ ∅)) = (𝑅 ∩ ∅)
4		in0 4325	. . . . . 6 ⊢ (𝑅 ∩ ∅) = ∅
5	3, 4	eqtri 2766	. . . . 5 ⊢ (𝑅 ∩ ( I ↾ ∅)) = ∅
6		xp0 6061	. . . . . . . . . 10 ⊢ (𝐴 × ∅) = ∅
7	6	ineq2i 4143	. . . . . . . . 9 ⊢ (𝑅 ∩ (𝐴 × ∅)) = (𝑅 ∩ ∅)
8	7, 4	eqtri 2766	. . . . . . . 8 ⊢ (𝑅 ∩ (𝐴 × ∅)) = ∅
9	8	coeq2i 5769	. . . . . . 7 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅)
10		co02 6164	. . . . . . 7 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅) = ∅
11	9, 10	eqtri 2766	. . . . . 6 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ∅
12		0ss 4330	. . . . . 6 ⊢ ∅ ⊆ 𝑅
13	11, 12	eqsstri 3955	. . . . 5 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅
14	5, 13	pm3.2i 471	. . . 4 ⊢ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)
15	1, 14	2th 263	. . 3 ⊢ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
16		poeq2 5507	. . . 4 ⊢ (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ 𝑅 Po ∅))
17		reseq2 5886	. . . . . . 7 ⊢ (𝐴 = ∅ → ( I ↾ 𝐴) = ( I ↾ ∅))
18	17	ineq2d 4146	. . . . . 6 ⊢ (𝐴 = ∅ → (𝑅 ∩ ( I ↾ 𝐴)) = (𝑅 ∩ ( I ↾ ∅)))
19	18	eqeq1d 2740	. . . . 5 ⊢ (𝐴 = ∅ → ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ (𝑅 ∩ ( I ↾ ∅)) = ∅))
20		xpeq2 5610	. . . . . . . 8 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (𝐴 × ∅))
21	20	ineq2d 4146	. . . . . . 7 ⊢ (𝐴 = ∅ → (𝑅 ∩ (𝐴 × 𝐴)) = (𝑅 ∩ (𝐴 × ∅)))
22	21	coeq2d 5771	. . . . . 6 ⊢ (𝐴 = ∅ → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))))
23	22	sseq1d 3952	. . . . 5 ⊢ (𝐴 = ∅ → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
24	19, 23	anbi12d 631	. . . 4 ⊢ (𝐴 = ∅ → (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)))
25	16, 24	bibi12d 346	. . 3 ⊢ (𝐴 = ∅ → ((𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) ↔ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))))
26	15, 25	mpbiri 257	. 2 ⊢ (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
27		r19.28zv 4431	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → (∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
28	27	ralbidv 3112	. . . . . 6 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
29		r19.28zv 4431	. . . . . 6 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
30	28, 29	bitrd 278	. . . . 5 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
31	30	ralbidv 3112	. . . 4 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
32		r19.26 3095	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
33	31, 32	bitrdi 287	. . 3 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
34		df-po 5503	. . 3 ⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
35		disj 4381	. . . . 5 ⊢ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑤 ∈ 𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴))
36		df-ral 3069	. . . . 5 ⊢ (∀𝑤 ∈ 𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
37		opex 5379	. . . . . . . . . 10 ⊢ ⟨𝑥, 𝑥⟩ ∈ V
38		eleq1 2826	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ 𝑅 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅))
39		df-br 5075	. . . . . . . . . . . 12 ⊢ (𝑥𝑅𝑥 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅)
40	38, 39	bitr4di 289	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ 𝑅 ↔ 𝑥𝑅𝑥))
41		eleq1 2826	. . . . . . . . . . . . 13 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴)))
42		opelidres 5903	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ V → (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥 ∈ 𝐴))
43	42	elv 3438	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥 ∈ 𝐴)
44	41, 43	bitrdi 287	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ 𝑥 ∈ 𝐴))
45	44	notbid 318	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴))
46	40, 45	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → ((𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ (𝑥𝑅𝑥 → ¬ 𝑥 ∈ 𝐴)))
47	37, 46	spcv 3544	. . . . . . . . 9 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝑅𝑥 → ¬ 𝑥 ∈ 𝐴))
48	47	con2d 134	. . . . . . . 8 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
49	48	alrimiv 1930	. . . . . . 7 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
50		relres 5920	. . . . . . . . . . . 12 ⊢ Rel ( I ↾ 𝐴)
51		elrel 5708	. . . . . . . . . . . 12 ⊢ ((Rel ( I ↾ 𝐴) ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
52	50, 51	mpan 687	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ( I ↾ 𝐴) → ∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
53	52	ancri 550	. . . . . . . . . 10 ⊢ (𝑤 ∈ ( I ↾ 𝐴) → (∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)))
54		eleq1 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
55		breq12 5079	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥𝑅𝑥 ↔ 𝑦𝑅𝑦))
56	55	anidms 567	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑥𝑅𝑥 ↔ 𝑦𝑅𝑦))
57	56	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑦𝑅𝑦))
58	54, 57	imbi12d 345	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) ↔ (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦)))
59	58	spvv 2000	. . . . . . . . . . . . . 14 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦))
60		breq2 5078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑦 ↔ 𝑦𝑅𝑧))
61	60	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → (¬ 𝑦𝑅𝑦 ↔ ¬ 𝑦𝑅𝑧))
62	61	imbi2d 341	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) ↔ (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑧)))
63	62	biimpcd 248	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) → (𝑦 = 𝑧 → (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑧)))
64	63	impcomd 412	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) → ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
65	59, 64	syl 17	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
66		eleq1 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴)))
67		vex 3436	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
68	67	brresi 5900	. . . . . . . . . . . . . . . 16 ⊢ (𝑦( I ↾ 𝐴)𝑧 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 I 𝑧))
69		df-br 5075	. . . . . . . . . . . . . . . 16 ⊢ (𝑦( I ↾ 𝐴)𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
70	67	ideq 5761	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 I 𝑧 ↔ 𝑦 = 𝑧)
71	70	anbi2i 623	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 I 𝑧) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧))
72	68, 69, 71	3bitr3ri 302	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
73	66, 72	bitr4di 289	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧)))
74		eleq1 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ 𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
75		df-br 5075	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑅𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅)
76	74, 75	bitr4di 289	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ 𝑅 ↔ 𝑦𝑅𝑧))
77	76	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (¬ 𝑤 ∈ 𝑅 ↔ ¬ 𝑦𝑅𝑧))
78	73, 77	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧)))
79	65, 78	syl5ibrcom 246	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅)))
80	79	exlimdvv 1937	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅)))
81	80	impd 411	. . . . . . . . . 10 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ((∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ¬ 𝑤 ∈ 𝑅))
82	53, 81	syl5 34	. . . . . . . . 9 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅))
83	82	con2d 134	. . . . . . . 8 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
84	83	alrimiv 1930	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
85	49, 84	impbii 208	. . . . . 6 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
86		df-ral 3069	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
87	85, 86	bitr4i 277	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥)
88	35, 36, 87	3bitri 297	. . . 4 ⊢ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥)
89		ralcom 3166	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
90		r19.23v 3208	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
91	90	ralbii 3092	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
92	89, 91	bitri 274	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
93	92	ralbii 3092	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
94		brin 5126	. . . . . . . . . . . 12 ⊢ (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ↔ (𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦))
95		brin 5126	. . . . . . . . . . . 12 ⊢ (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧 ↔ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧))
96	94, 95	anbi12i 627	. . . . . . . . . . 11 ⊢ ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)))
97		an4 653	. . . . . . . . . . . 12 ⊢ (((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧)))
98		ancom 461	. . . . . . . . . . . 12 ⊢ (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
99		ancom 461	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴))
100	99	anbi1i 624	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
101		brxp 5636	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝐴 × 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴))
102		brxp 5636	. . . . . . . . . . . . . . 15 ⊢ (𝑦(𝐴 × 𝐴)𝑧 ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))
103	101, 102	anbi12i 627	. . . . . . . . . . . . . 14 ⊢ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
104		anandi 673	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
105	100, 103, 104	3bitr4i 303	. . . . . . . . . . . . 13 ⊢ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ↔ (𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
106	105	anbi1i 624	. . . . . . . . . . . 12 ⊢ (((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
107	97, 98, 106	3bitri 297	. . . . . . . . . . 11 ⊢ (((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
108		anass 469	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ (𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
109	96, 107, 108	3bitri 297	. . . . . . . . . 10 ⊢ ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ (𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
110	109	exbii 1850	. . . . . . . . 9 ⊢ (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
111		vex 3436	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
112	111, 67	brco 5779	. . . . . . . . . 10 ⊢ (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧))
113		df-br 5075	. . . . . . . . . 10 ⊢ (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
114	112, 113	bitr3i 276	. . . . . . . . 9 ⊢ (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
115		df-rex 3070	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
116		r19.42v 3279	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
117	115, 116	bitr3i 276	. . . . . . . . 9 ⊢ (∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
118	110, 114, 117	3bitr3ri 302	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
119		df-br 5075	. . . . . . . 8 ⊢ (𝑥𝑅𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑅)
120	118, 119	imbi12i 351	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ (⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
121	120	2albii 1823	. . . . . 6 ⊢ (∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
122		r2al 3118	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
123		impexp 451	. . . . . . . 8 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
124	123	2albii 1823	. . . . . . 7 ⊢ (∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
125	122, 124	bitr4i 277	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
126		relco 6148	. . . . . . 7 ⊢ Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))
127		ssrel 5693	. . . . . . 7 ⊢ (Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅)))
128	126, 127	ax-mp 5	. . . . . 6 ⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
129	121, 125, 128	3bitr4i 303	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)
130	93, 129	bitr2i 275	. . . 4 ⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
131	88, 130	anbi12i 627	. . 3 ⊢ (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
132	33, 34, 131	3bitr4g 314	. 2 ⊢ (𝐴 ≠ ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
133	26, 132	pm2.61ine 3028	1 ⊢ (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  Vcvv 3432   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  ⟨cop 4567   class class class wbr 5074   I cid 5488   Po wpo 5501   × cxp 5587   ↾ cres 5591   ∘ ccom 5593  Rel wrel 5594

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  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-br 5075  df-opab 5137  df-id 5489  df-po 5503  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-res 5601

This theorem is referenced by:  predpo  6226