Theorem dfpo2 30898

Description: Quantifier free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.)

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 4974	. . . 4 ⊢ 𝑅 Po ∅
2		res0 5321	. . . . . . 7 ⊢ ( I ↾ ∅) = ∅
3	2	ineq2i 3773	. . . . . 6 ⊢ (𝑅 ∩ ( I ↾ ∅)) = (𝑅 ∩ ∅)
4		in0 3920	. . . . . 6 ⊢ (𝑅 ∩ ∅) = ∅
5	3, 4	eqtri 2632	. . . . 5 ⊢ (𝑅 ∩ ( I ↾ ∅)) = ∅
6		xp0 5471	. . . . . . . . . 10 ⊢ (𝐴 × ∅) = ∅
7	6	ineq2i 3773	. . . . . . . . 9 ⊢ (𝑅 ∩ (𝐴 × ∅)) = (𝑅 ∩ ∅)
8	7, 4	eqtri 2632	. . . . . . . 8 ⊢ (𝑅 ∩ (𝐴 × ∅)) = ∅
9	8	coeq2i 5204	. . . . . . 7 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅)
10		co02 5566	. . . . . . 7 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅) = ∅
11	9, 10	eqtri 2632	. . . . . 6 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ∅
12		0ss 3924	. . . . . 6 ⊢ ∅ ⊆ 𝑅
13	11, 12	eqsstri 3598	. . . . 5 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅
14	5, 13	pm3.2i 470	. . . 4 ⊢ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)
15	1, 14	2th 253	. . 3 ⊢ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
16		poeq2 4963	. . . 4 ⊢ (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ 𝑅 Po ∅))
17		reseq2 5312	. . . . . . 7 ⊢ (𝐴 = ∅ → ( I ↾ 𝐴) = ( I ↾ ∅))
18	17	ineq2d 3776	. . . . . 6 ⊢ (𝐴 = ∅ → (𝑅 ∩ ( I ↾ 𝐴)) = (𝑅 ∩ ( I ↾ ∅)))
19	18	eqeq1d 2612	. . . . 5 ⊢ (𝐴 = ∅ → ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ (𝑅 ∩ ( I ↾ ∅)) = ∅))
20		xpeq2 5053	. . . . . . . 8 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (𝐴 × ∅))
21	20	ineq2d 3776	. . . . . . 7 ⊢ (𝐴 = ∅ → (𝑅 ∩ (𝐴 × 𝐴)) = (𝑅 ∩ (𝐴 × ∅)))
22	21	coeq2d 5206	. . . . . 6 ⊢ (𝐴 = ∅ → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))))
23	22	sseq1d 3595	. . . . 5 ⊢ (𝐴 = ∅ → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
24	19, 23	anbi12d 743	. . . 4 ⊢ (𝐴 = ∅ → (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)))
25	16, 24	bibi12d 334	. . 3 ⊢ (𝐴 = ∅ → ((𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) ↔ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))))
26	15, 25	mpbiri 247	. 2 ⊢ (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
27		r19.28zv 4018	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → (∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
28	27	ralbidv 2969	. . . . . 6 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
29		r19.28zv 4018	. . . . . 6 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
30	28, 29	bitrd 267	. . . . 5 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
31	30	ralbidv 2969	. . . 4 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
32		r19.26 3046	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
33	31, 32	syl6bb 275	. . 3 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
34		df-po 4959	. . 3 ⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
35		disj 3969	. . . . 5 ⊢ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑤 ∈ 𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴))
36		df-ral 2901	. . . . 5 ⊢ (∀𝑤 ∈ 𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
37		opex 4859	. . . . . . . . . 10 ⊢ ⟨𝑥, 𝑥⟩ ∈ V
38		eleq1 2676	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ 𝑅 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅))
39		df-br 4584	. . . . . . . . . . . 12 ⊢ (𝑥𝑅𝑥 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅)
40	38, 39	syl6bbr 277	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ 𝑅 ↔ 𝑥𝑅𝑥))
41		eleq1 2676	. . . . . . . . . . . . 13 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴)))
42		vex 3176	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
43		ididg 5197	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ V → 𝑥 I 𝑥)
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 𝑥 I 𝑥
45	42	brres 5323	. . . . . . . . . . . . . . 15 ⊢ (𝑥( I ↾ 𝐴)𝑥 ↔ (𝑥 I 𝑥 ∧ 𝑥 ∈ 𝐴))
46	44, 45	mpbiran 955	. . . . . . . . . . . . . 14 ⊢ (𝑥( I ↾ 𝐴)𝑥 ↔ 𝑥 ∈ 𝐴)
47		df-br 4584	. . . . . . . . . . . . . 14 ⊢ (𝑥( I ↾ 𝐴)𝑥 ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴))
48	46, 47	bitr3i 265	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴))
49	41, 48	syl6bbr 277	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ 𝑥 ∈ 𝐴))
50	49	notbid 307	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴))
51	40, 50	imbi12d 333	. . . . . . . . . 10 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → ((𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ (𝑥𝑅𝑥 → ¬ 𝑥 ∈ 𝐴)))
52	37, 51	spcv 3272	. . . . . . . . 9 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝑅𝑥 → ¬ 𝑥 ∈ 𝐴))
53	52	con2d 128	. . . . . . . 8 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
54	53	alrimiv 1842	. . . . . . 7 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
55		relres 5346	. . . . . . . . . . . 12 ⊢ Rel ( I ↾ 𝐴)
56		elrel 5145	. . . . . . . . . . . 12 ⊢ ((Rel ( I ↾ 𝐴) ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
57	55, 56	mpan 702	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ( I ↾ 𝐴) → ∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
58	57	ancri 573	. . . . . . . . . 10 ⊢ (𝑤 ∈ ( I ↾ 𝐴) → (∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)))
59		eleq1 2676	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
60		breq12 4588	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥𝑅𝑥 ↔ 𝑦𝑅𝑦))
61	60	anidms 675	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑥𝑅𝑥 ↔ 𝑦𝑅𝑦))
62	61	notbid 307	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑦𝑅𝑦))
63	59, 62	imbi12d 333	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) ↔ (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦)))
64	63	spv 2248	. . . . . . . . . . . . . 14 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦))
65		breq2 4587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑦 ↔ 𝑦𝑅𝑧))
66	65	notbid 307	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → (¬ 𝑦𝑅𝑦 ↔ ¬ 𝑦𝑅𝑧))
67	66	imbi2d 329	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) ↔ (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑧)))
68	67	biimpcd 238	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) → (𝑦 = 𝑧 → (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑧)))
69	68	impd 446	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) → ((𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦𝑅𝑧))
70	64, 69	syl 17	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ((𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦𝑅𝑧))
71		eleq1 2676	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴)))
72		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
73	72	brres 5323	. . . . . . . . . . . . . . . 16 ⊢ (𝑦( I ↾ 𝐴)𝑧 ↔ (𝑦 I 𝑧 ∧ 𝑦 ∈ 𝐴))
74		df-br 4584	. . . . . . . . . . . . . . . 16 ⊢ (𝑦( I ↾ 𝐴)𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
75	72	ideq 5196	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 I 𝑧 ↔ 𝑦 = 𝑧)
76	75	anbi1i 727	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 I 𝑧 ∧ 𝑦 ∈ 𝐴) ↔ (𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴))
77	73, 74, 76	3bitr3ri 290	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
78	71, 77	syl6bbr 277	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ (𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴)))
79		eleq1 2676	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ 𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
80		df-br 4584	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑅𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅)
81	79, 80	syl6bbr 277	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ 𝑅 ↔ 𝑦𝑅𝑧))
82	81	notbid 307	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (¬ 𝑤 ∈ 𝑅 ↔ ¬ 𝑦𝑅𝑧))
83	78, 82	imbi12d 333	. . . . . . . . . . . . 13 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅) ↔ ((𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦𝑅𝑧)))
84	70, 83	syl5ibrcom 236	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅)))
85	84	exlimdvv 1849	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅)))
86	85	impd 446	. . . . . . . . . 10 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ((∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ¬ 𝑤 ∈ 𝑅))
87	58, 86	syl5 33	. . . . . . . . 9 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅))
88	87	con2d 128	. . . . . . . 8 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
89	88	alrimiv 1842	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
90	54, 89	impbii 198	. . . . . 6 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
91		df-ral 2901	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
92	90, 91	bitr4i 266	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥)
93	35, 36, 92	3bitri 285	. . . 4 ⊢ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥)
94		ralcom 3079	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
95		r19.23v 3005	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
96	95	ralbii 2963	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
97	94, 96	bitri 263	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
98	97	ralbii 2963	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
99		brin 4634	. . . . . . . . . . . 12 ⊢ (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ↔ (𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦))
100		brin 4634	. . . . . . . . . . . 12 ⊢ (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧 ↔ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧))
101	99, 100	anbi12i 729	. . . . . . . . . . 11 ⊢ ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)))
102		an4 861	. . . . . . . . . . . 12 ⊢ (((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧)))
103		ancom 465	. . . . . . . . . . . 12 ⊢ (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
104		ancom 465	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴))
105	104	anbi1i 727	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
106		brxp 5071	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝐴 × 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴))
107		brxp 5071	. . . . . . . . . . . . . . 15 ⊢ (𝑦(𝐴 × 𝐴)𝑧 ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))
108	106, 107	anbi12i 729	. . . . . . . . . . . . . 14 ⊢ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
109		anandi 867	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
110	105, 108, 109	3bitr4i 291	. . . . . . . . . . . . 13 ⊢ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ↔ (𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
111	110	anbi1i 727	. . . . . . . . . . . 12 ⊢ (((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
112	102, 103, 111	3bitri 285	. . . . . . . . . . 11 ⊢ (((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
113		anass 679	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ (𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
114	101, 112, 113	3bitri 285	. . . . . . . . . 10 ⊢ ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ (𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
115	114	exbii 1764	. . . . . . . . 9 ⊢ (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
116	42, 72	brco 5214	. . . . . . . . . 10 ⊢ (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧))
117		df-br 4584	. . . . . . . . . 10 ⊢ (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
118	116, 117	bitr3i 265	. . . . . . . . 9 ⊢ (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
119		df-rex 2902	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
120		r19.42v 3073	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
121	119, 120	bitr3i 265	. . . . . . . . 9 ⊢ (∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
122	115, 118, 121	3bitr3ri 290	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
123		df-br 4584	. . . . . . . 8 ⊢ (𝑥𝑅𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑅)
124	122, 123	imbi12i 339	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ (⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
125	124	2albii 1738	. . . . . 6 ⊢ (∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
126		r2al 2923	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
127		impexp 461	. . . . . . . 8 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
128	127	2albii 1738	. . . . . . 7 ⊢ (∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
129	126, 128	bitr4i 266	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
130		relco 5550	. . . . . . 7 ⊢ Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))
131		ssrel 5130	. . . . . . 7 ⊢ (Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅)))
132	130, 131	ax-mp 5	. . . . . 6 ⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
133	125, 129, 132	3bitr4i 291	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)
134	98, 133	bitr2i 264	. . . 4 ⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
135	93, 134	anbi12i 729	. . 3 ⊢ (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
136	33, 34, 135	3bitr4g 302	. 2 ⊢ (𝐴 ≠ ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
137	26, 136	pm2.61ine 2865	1 ⊢ (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ⟨cop 4131   class class class wbr 4583   I cid 4948   Po wpo 4957   × cxp 5036   ↾ cres 5040   ∘ ccom 5042  Rel wrel 5043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-id 4953  df-po 4959  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-res 5050

This theorem is referenced by: (None)