Theorem dfpo2 6247

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 5543	. . . 4 ⊢ 𝑅 Po ∅
2		res0 5935	. . . . . . 7 ⊢ ( I ↾ ∅) = ∅
3	2	ineq2i 4146	. . . . . 6 ⊢ (𝑅 ∩ ( I ↾ ∅)) = (𝑅 ∩ ∅)
4		in0 4323	. . . . . 6 ⊢ (𝑅 ∩ ∅) = ∅
5	3, 4	eqtri 2762	. . . . 5 ⊢ (𝑅 ∩ ( I ↾ ∅)) = ∅
6		xp0 5718	. . . . . . . . . 10 ⊢ (𝐴 × ∅) = ∅
7	6	ineq2i 4146	. . . . . . . . 9 ⊢ (𝑅 ∩ (𝐴 × ∅)) = (𝑅 ∩ ∅)
8	7, 4	eqtri 2762	. . . . . . . 8 ⊢ (𝑅 ∩ (𝐴 × ∅)) = ∅
9	8	coeq2i 5802	. . . . . . 7 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅)
10		co02 6212	. . . . . . 7 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅) = ∅
11	9, 10	eqtri 2762	. . . . . 6 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ∅
12		0ss 4328	. . . . . 6 ⊢ ∅ ⊆ 𝑅
13	11, 12	eqsstri 3961	. . . . 5 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅
14	5, 13	pm3.2i 471	. . . 4 ⊢ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)
15	1, 14	2th 265	. . 3 ⊢ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
16		poeq2 5530	. . . 4 ⊢ (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ 𝑅 Po ∅))
17		reseq2 5926	. . . . . . 7 ⊢ (𝐴 = ∅ → ( I ↾ 𝐴) = ( I ↾ ∅))
18	17	ineq2d 4149	. . . . . 6 ⊢ (𝐴 = ∅ → (𝑅 ∩ ( I ↾ 𝐴)) = (𝑅 ∩ ( I ↾ ∅)))
19	18	eqeq1d 2741	. . . . 5 ⊢ (𝐴 = ∅ → ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ (𝑅 ∩ ( I ↾ ∅)) = ∅))
20		xpeq2 5639	. . . . . . . 8 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (𝐴 × ∅))
21	20	ineq2d 4149	. . . . . . 7 ⊢ (𝐴 = ∅ → (𝑅 ∩ (𝐴 × 𝐴)) = (𝑅 ∩ (𝐴 × ∅)))
22	21	coeq2d 5804	. . . . . 6 ⊢ (𝐴 = ∅ → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))))
23	22	sseq1d 3946	. . . . 5 ⊢ (𝐴 = ∅ → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
24	19, 23	anbi12d 638	. . . 4 ⊢ (𝐴 = ∅ → (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)))
25	16, 24	bibi12d 346	. . 3 ⊢ (𝐴 = ∅ → ((𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) ↔ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))))
26	15, 25	mpbiri 259	. 2 ⊢ (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
27		r19.28zv 4434	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → (∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
28	27	ralbidv 3162	. . . . . 6 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
29		r19.28zv 4434	. . . . . 6 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
30	28, 29	bitrd 280	. . . . 5 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
31	30	ralbidv 3162	. . . 4 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
32		r19.26 3099	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
33	31, 32	bitrdi 288	. . 3 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
34		df-po 5526	. . 3 ⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
35		disj 4378	. . . . 5 ⊢ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑤 ∈ 𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴))
36		df-ral 3054	. . . . 5 ⊢ (∀𝑤 ∈ 𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
37		opex 5403	. . . . . . . . . 10 ⊢ ⟨𝑥, 𝑥⟩ ∈ V
38		eleq1 2827	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ 𝑅 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅))
39		df-br 5073	. . . . . . . . . . . 12 ⊢ (𝑥𝑅𝑥 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅)
40	38, 39	bitr4di 290	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ 𝑅 ↔ 𝑥𝑅𝑥))
41		eleq1 2827	. . . . . . . . . . . . 13 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴)))
42		opelidres 5943	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ V → (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥 ∈ 𝐴))
43	42	elv 3436	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥 ∈ 𝐴)
44	41, 43	bitrdi 288	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ 𝑥 ∈ 𝐴))
45	44	notbid 319	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → (¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴))
46	40, 45	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ → ((𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ (𝑥𝑅𝑥 → ¬ 𝑥 ∈ 𝐴)))
47	37, 46	spcv 3543	. . . . . . . . 9 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝑅𝑥 → ¬ 𝑥 ∈ 𝐴))
48	47	con2d 134	. . . . . . . 8 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
49	48	alrimiv 1934	. . . . . . 7 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
50		relres 5957	. . . . . . . . . . . 12 ⊢ Rel ( I ↾ 𝐴)
51		elrel 5741	. . . . . . . . . . . 12 ⊢ ((Rel ( I ↾ 𝐴) ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
52	50, 51	mpan 696	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ( I ↾ 𝐴) → ∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
53	52	ancri 554	. . . . . . . . . 10 ⊢ (𝑤 ∈ ( I ↾ 𝐴) → (∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)))
54		eleq1 2827	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
55		breq12 5077	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥𝑅𝑥 ↔ 𝑦𝑅𝑦))
56	55	anidms 571	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑥𝑅𝑥 ↔ 𝑦𝑅𝑦))
57	56	notbid 319	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑦𝑅𝑦))
58	54, 57	imbi12d 345	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) ↔ (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦)))
59	58	spvv 1995	. . . . . . . . . . . . . 14 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦))
60		breq2 5076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑦 ↔ 𝑦𝑅𝑧))
61	60	notbid 319	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → (¬ 𝑦𝑅𝑦 ↔ ¬ 𝑦𝑅𝑧))
62	61	imbi2d 341	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) ↔ (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑧)))
63	62	biimpcd 250	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) → (𝑦 = 𝑧 → (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑧)))
64	63	impcomd 412	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) → ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
65	59, 64	syl 17	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
66		eleq1 2827	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴)))
67		vex 3435	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
68	67	brresi 5940	. . . . . . . . . . . . . . . 16 ⊢ (𝑦( I ↾ 𝐴)𝑧 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 I 𝑧))
69		df-br 5073	. . . . . . . . . . . . . . . 16 ⊢ (𝑦( I ↾ 𝐴)𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
70	67	ideq 5794	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 I 𝑧 ↔ 𝑦 = 𝑧)
71	70	anbi2i 629	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 I 𝑧) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧))
72	68, 69, 71	3bitr3ri 303	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
73	66, 72	bitr4di 290	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧)))
74		eleq1 2827	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ 𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
75		df-br 5073	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑅𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅)
76	74, 75	bitr4di 290	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ 𝑅 ↔ 𝑦𝑅𝑧))
77	76	notbid 319	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (¬ 𝑤 ∈ 𝑅 ↔ ¬ 𝑦𝑅𝑧))
78	73, 77	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧)))
79	65, 78	syl5ibrcom 248	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅)))
80	79	exlimdvv 1941	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅)))
81	80	impd 411	. . . . . . . . . 10 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ((∃𝑦∃𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ¬ 𝑤 ∈ 𝑅))
82	53, 81	syl5 34	. . . . . . . . 9 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅))
83	82	con2d 134	. . . . . . . 8 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
84	83	alrimiv 1934	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
85	49, 84	impbii 210	. . . . . 6 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
86		df-ral 3054	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥))
87	85, 86	bitr4i 279	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥)
88	35, 36, 87	3bitri 298	. . . 4 ⊢ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥)
89		ralcom 3267	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
90		r19.23v 3166	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
91	90	ralbii 3085	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
92	89, 91	bitri 276	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
93	92	ralbii 3085	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
94		brin 5124	. . . . . . . . . . . 12 ⊢ (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ↔ (𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦))
95		brin 5124	. . . . . . . . . . . 12 ⊢ (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧 ↔ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧))
96	94, 95	anbi12i 634	. . . . . . . . . . 11 ⊢ ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)))
97		an4 662	. . . . . . . . . . . 12 ⊢ (((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧)))
98		ancom 461	. . . . . . . . . . . 12 ⊢ (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
99		ancom 461	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴))
100	99	anbi1i 630	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
101		brxp 5667	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝐴 × 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴))
102		brxp 5667	. . . . . . . . . . . . . . 15 ⊢ (𝑦(𝐴 × 𝐴)𝑧 ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))
103	101, 102	anbi12i 634	. . . . . . . . . . . . . 14 ⊢ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
104		anandi 682	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
105	100, 103, 104	3bitr4i 304	. . . . . . . . . . . . 13 ⊢ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ↔ (𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)))
106	105	anbi1i 630	. . . . . . . . . . . 12 ⊢ (((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
107	97, 98, 106	3bitri 298	. . . . . . . . . . 11 ⊢ (((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
108		anass 469	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ (𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
109	96, 107, 108	3bitri 298	. . . . . . . . . 10 ⊢ ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ (𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
110	109	exbii 1855	. . . . . . . . 9 ⊢ (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
111		vex 3435	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
112	111, 67	brco 5812	. . . . . . . . . 10 ⊢ (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧))
113		df-br 5073	. . . . . . . . . 10 ⊢ (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
114	112, 113	bitr3i 278	. . . . . . . . 9 ⊢ (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
115		df-rex 3064	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))))
116		r19.42v 3171	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
117	115, 116	bitr3i 278	. . . . . . . . 9 ⊢ (∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
118	110, 114, 117	3bitr3ri 303	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
119		df-br 5073	. . . . . . . 8 ⊢ (𝑥𝑅𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑅)
120	118, 119	imbi12i 351	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ (⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
121	120	2albii 1827	. . . . . 6 ⊢ (∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
122		r2al 3175	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
123		impexp 451	. . . . . . . 8 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
124	123	2albii 1827	. . . . . . 7 ⊢ (∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
125	122, 124	bitr4i 279	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
126		relco 6060	. . . . . . 7 ⊢ Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))
127		ssrel 5726	. . . . . . 7 ⊢ (Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅)))
128	126, 127	ax-mp 5	. . . . . 6 ⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
129	121, 125, 128	3bitr4i 304	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)
130	93, 129	bitr2i 277	. . . 4 ⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
131	88, 130	anbi12i 634	. . 3 ⊢ (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
132	33, 34, 131	3bitr4g 315	. 2 ⊢ (𝐴 ≠ ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
133	26, 132	pm2.61ine 3017	1 ⊢ (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545   = wceq 1547  ∃wex 1786   ∈ wcel 2119   ≠ wne 2934  ∀wral 3053  ∃wrex 3063  Vcvv 3431   ∩ cin 3882   ⊆ wss 3883  ∅c0 4261  ⟨cop 4561   class class class wbr 5072   I cid 5512   Po wpo 5524   × cxp 5616   ↾ cres 5620   ∘ ccom 5622  Rel wrel 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-id 5513  df-po 5526  df-xp 5624  df-rel 5625  df-co 5627  df-res 5630

This theorem is referenced by:  predpo  6274