Theorem ordtrest2NEWlem 33198

Description: Lemma for ordtrest2NEW 33199. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.)

Hypotheses

Ref	Expression
ordtNEW.b	⊢ 𝐵 = (Base‘𝐾)
ordtNEW.l	⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
ordtrest2NEW.2	⊢ (𝜑 → 𝐾 ∈ Toset)
ordtrest2NEW.3	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
ordtrest2NEW.4	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴)

Assertion

Ref	Expression
ordtrest2NEWlem	⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))

Distinct variable groups:   𝑥,𝑦, ≤   𝑥,𝐵,𝑦   𝑥,𝐾,𝑦   𝑥,𝐴,𝑦,𝑣,𝑤,𝑧   𝑣, ≤   𝑥,𝑤,𝑧,𝑦, ≤   𝑣,𝐴,𝑤,𝑧   𝑣,𝐵,𝑤,𝑧   𝜑,𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑤,𝑣)   𝐾(𝑧,𝑤,𝑣)

Proof of Theorem ordtrest2NEWlem

Step	Hyp	Ref	Expression
1		inrab2 4308	. . . . 5 ⊢ ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) = {𝑤 ∈ (𝐵 ∩ 𝐴) ∣ ¬ 𝑤 ≤ 𝑧}
2		ordtrest2NEW.3	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3		sseqin2 4216	. . . . . . . 8 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)
4	2, 3	sylib 217	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∩ 𝐴) = 𝐴)
5	4	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐵 ∩ 𝐴) = 𝐴)
6		rabeq 3444	. . . . . 6 ⊢ ((𝐵 ∩ 𝐴) = 𝐴 → {𝑤 ∈ (𝐵 ∩ 𝐴) ∣ ¬ 𝑤 ≤ 𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧})
7	5, 6	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → {𝑤 ∈ (𝐵 ∩ 𝐴) ∣ ¬ 𝑤 ≤ 𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧})
8	1, 7	eqtrid 2782	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧})
9		ordtNEW.l	. . . . . . . . . . . . 13 ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
10		fvex 6905	. . . . . . . . . . . . . 14 ⊢ (le‘𝐾) ∈ V
11	10	inex1 5318	. . . . . . . . . . . . 13 ⊢ ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
12	9, 11	eqeltri 2827	. . . . . . . . . . . 12 ⊢ ≤ ∈ V
13	12	inex1 5318	. . . . . . . . . . 11 ⊢ ( ≤ ∩ (𝐴 × 𝐴)) ∈ V
14	13	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ( ≤ ∩ (𝐴 × 𝐴)) ∈ V)
15		eqid 2730	. . . . . . . . . . 11 ⊢ dom ( ≤ ∩ (𝐴 × 𝐴)) = dom ( ≤ ∩ (𝐴 × 𝐴))
16	15	ordttopon 22919	. . . . . . . . . 10 ⊢ (( ≤ ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom ( ≤ ∩ (𝐴 × 𝐴))))
17	14, 16	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom ( ≤ ∩ (𝐴 × 𝐴))))
18		ordtrest2NEW.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Toset)
19		tospos 18379	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Toset → 𝐾 ∈ Poset)
20		posprs 18275	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset )
21	18, 19, 20	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ Proset )
22		ordtNEW.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝐾)
23	22, 9	prsssdm 33193	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴)
24	21, 2, 23	syl2anc 582	. . . . . . . . . 10 ⊢ (𝜑 → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴)
25	24	fveq2d 6896	. . . . . . . . 9 ⊢ (𝜑 → (TopOn‘dom ( ≤ ∩ (𝐴 × 𝐴))) = (TopOn‘𝐴))
26	17, 25	eleqtrd 2833	. . . . . . . 8 ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴))
27		toponmax 22650	. . . . . . . 8 ⊢ ((ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴) → 𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
28	26, 27	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
29	28	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
30		rabid2 3462	. . . . . . 7 ⊢ (𝐴 = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ↔ ∀𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧)
31		eleq1 2819	. . . . . . 7 ⊢ (𝐴 = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} → (𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
32	30, 31	sylbir 234	. . . . . 6 ⊢ (∀𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧 → (𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
33	29, 32	syl5ibcom 244	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (∀𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
34		dfrex2 3071	. . . . . . 7 ⊢ (∃𝑤 ∈ 𝐴 𝑤 ≤ 𝑧 ↔ ¬ ∀𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧)
35		breq1 5152	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝑤 ≤ 𝑧 ↔ 𝑥 ≤ 𝑧))
36	35	cbvrexvw 3233	. . . . . . 7 ⊢ (∃𝑤 ∈ 𝐴 𝑤 ≤ 𝑧 ↔ ∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑧)
37	34, 36	bitr3i 276	. . . . . 6 ⊢ (¬ ∀𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧 ↔ ∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑧)
38		ordttop 22926	. . . . . . . . . . . . 13 ⊢ (( ≤ ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top)
39	14, 38	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top)
40	39	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top)
41		0opn 22628	. . . . . . . . . . 11 ⊢ ((ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top → ∅ ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
42	40, 41	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ∅ ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
43	42	adantr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → ∅ ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
44		eleq1 2819	. . . . . . . . 9 ⊢ ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} = ∅ → ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ ∅ ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
45	43, 44	syl5ibrcom 246	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} = ∅ → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
46		rabn0 4386	. . . . . . . . . 10 ⊢ ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ≠ ∅ ↔ ∃𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧)
47		breq1 5152	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑦 → (𝑤 ≤ 𝑧 ↔ 𝑦 ≤ 𝑧))
48	47	notbid 317	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑦 → (¬ 𝑤 ≤ 𝑧 ↔ ¬ 𝑦 ≤ 𝑧))
49	48	cbvrexvw 3233	. . . . . . . . . 10 ⊢ (∃𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑧)
50	46, 49	bitri 274	. . . . . . . . 9 ⊢ ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ≠ ∅ ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑧)
51	18	ad3antrrr 726	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Toset)
52	2	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → 𝐴 ⊆ 𝐵)
53	52	sselda 3983	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐵)
54		simpllr 772	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐵)
55	22, 9	trleile 32406	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Toset ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦 ≤ 𝑧 ∨ 𝑧 ≤ 𝑦))
56	51, 53, 54, 55	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → (𝑦 ≤ 𝑧 ∨ 𝑧 ≤ 𝑦))
57	56	ord 860	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → (¬ 𝑦 ≤ 𝑧 → 𝑧 ≤ 𝑦))
58		an4 652	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)))
59		ordtrest2NEW.4	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴)
60		rabss 4070	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴 ↔ ∀𝑧 ∈ 𝐵 ((𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) → 𝑧 ∈ 𝐴))
61	59, 60	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ∀𝑧 ∈ 𝐵 ((𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) → 𝑧 ∈ 𝐴))
62	61	r19.21bi 3246	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) → 𝑧 ∈ 𝐴))
63	62	an32s 648	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) → 𝑧 ∈ 𝐴))
64	63	impr 453	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))) → 𝑧 ∈ 𝐴)
65	58, 64	sylan2b 592	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → 𝑧 ∈ 𝐴)
66		brinxp 5755	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑤 ≤ 𝑧 ↔ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧))
67	66	ancoms 457	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑤 ≤ 𝑧 ↔ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧))
68	67	notbid 317	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (¬ 𝑤 ≤ 𝑧 ↔ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧))
69	68	rabbidva 3437	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝐴 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧})
70	65, 69	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧})
71	24	ad2antrr 722	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴)
72		rabeq 3444	. . . . . . . . . . . . . . . 16 ⊢ (dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴 → {𝑤 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧})
73	71, 72	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → {𝑤 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧})
74	70, 73	eqtr4d 2773	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} = {𝑤 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧})
75	13	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → ( ≤ ∩ (𝐴 × 𝐴)) ∈ V)
76	65, 71	eleqtrrd 2834	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → 𝑧 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)))
77	15	ordtopn1 22920	. . . . . . . . . . . . . . 15 ⊢ ((( ≤ ∩ (𝐴 × 𝐴)) ∈ V ∧ 𝑧 ∈ dom ( ≤ ∩ (𝐴 × 𝐴))) → {𝑤 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
78	75, 76, 77	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → {𝑤 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
79	74, 78	eqeltrd 2831	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
80	79	anassrs 466	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦)) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
81	80	expr 455	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → (𝑧 ≤ 𝑦 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
82	57, 81	syld 47	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → (¬ 𝑦 ≤ 𝑧 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
83	82	rexlimdva 3153	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → (∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑧 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
84	50, 83	biimtrid 241	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ≠ ∅ → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
85	45, 84	pm2.61dne 3026	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
86	85	rexlimdvaa 3154	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑧 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
87	37, 86	biimtrid 241	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (¬ ∀𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
88	33, 87	pm2.61d 179	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
89	8, 88	eqeltrd 2831	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
90	89	ralrimiva 3144	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
91		fvex 6905	. . . . . . 7 ⊢ (Base‘𝐾) ∈ V
92	22, 91	eqeltri 2827	. . . . . 6 ⊢ 𝐵 ∈ V
93	92	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
94		rabexg 5332	. . . . 5 ⊢ (𝐵 ∈ V → {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∈ V)
95	93, 94	syl 17	. . . 4 ⊢ (𝜑 → {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∈ V)
96	95	ralrimivw 3148	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∈ V)
97		eqid 2730	. . . 4 ⊢ (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) = (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})
98		ineq1 4206	. . . . 5 ⊢ (𝑣 = {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} → (𝑣 ∩ 𝐴) = ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴))
99	98	eleq1d 2816	. . . 4 ⊢ (𝑣 = {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} → ((𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
100	97, 99	ralrnmptw 7096	. . 3 ⊢ (∀𝑧 ∈ 𝐵 {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∈ V → (∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ ∀𝑧 ∈ 𝐵 ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
101	96, 100	syl 17	. 2 ⊢ (𝜑 → (∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ ∀𝑧 ∈ 𝐵 ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
102	90, 101	mpbird 256	1 ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   = wceq 1539   ∈ wcel 2104   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  {crab 3430  Vcvv 3472   ∩ cin 3948   ⊆ wss 3949  ∅c0 4323   class class class wbr 5149   ↦ cmpt 5232   × cxp 5675  dom cdm 5677  ran crn 5678  ‘cfv 6544  Basecbs 17150  lecple 17210  ordTopcordt 17451   Proset cproset 18252  Posetcpo 18266  Tosetctos 18375  Topctop 22617  TopOnctopon 22634

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-fi 9410  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11452  df-neg 11453  df-nn 12219  df-2 12281  df-3 12282  df-4 12283  df-5 12284  df-6 12285  df-7 12286  df-8 12287  df-9 12288  df-dec 12684  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17151  df-ress 17180  df-ple 17223  df-topgen 17395  df-ordt 17453  df-proset 18254  df-poset 18272  df-toset 18376  df-top 22618  df-topon 22635  df-bases 22671

This theorem is referenced by:  ordtrest2NEW  33199