Theorem lautcvr

Description: Covering property of a lattice automorphism. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	lautcvr.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lautcvr.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	lautcvr.i	⊢ 𝐼 = ( LAut ‘ 𝐾 )
Assertion	lautcvr	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) 𝐶 ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lautcvr.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lautcvr.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3		lautcvr.i	⊢ 𝐼 = ( LAut ‘ 𝐾 )
4		eqid	⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
5	1 4 3	lautlt	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
6		simpll	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝐾 ∈ 𝐴 )
7		simplr1	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝐹 ∈ 𝐼 )
8		simplr2	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
9		simpr	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ 𝐵 )
10	1 4 3	lautlt	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ↔ ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑤 ) ) )
11	6 7 8 9 10	syl13anc	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ↔ ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑤 ) ) )
12		simplr3	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
13	1 4 3	lautlt	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑤 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑤 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ 𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
14	6 7 9 12 13	syl13anc	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑤 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ 𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
15	11 14	anbi12d	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑤 ) ∧ ( 𝐹 ‘ 𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) )
16	1 3	lautcl	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝐹 ∈ 𝐼 ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
17	6 7 9 16	syl21anc	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
18		breq2	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ↔ ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑤 ) ) )
19		breq1	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → ( 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ 𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
20	18 19	anbi12d	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → ( ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑤 ) ∧ ( 𝐹 ‘ 𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) )
21	20	rspcev	⊢ ( ( ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑤 ) ∧ ( 𝐹 ‘ 𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) → ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
22	21	ex	⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 → ( ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑤 ) ∧ ( 𝐹 ‘ 𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) → ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) )
23	17 22	syl	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑤 ) ∧ ( 𝐹 ‘ 𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) → ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) )
24	15 23	sylbid	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) )
25	24	rexlimdva	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ∃ 𝑤 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) )
26		simpll	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝐾 ∈ 𝐴 )
27		simplr1	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝐹 ∈ 𝐼 )
28		simplr2	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
29	1 3	laut1o	⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝐹 ∈ 𝐼 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
30	26 27 29	syl2anc	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
31		f1ocnvdm	⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
32	30 31	sylancom	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
33	1 4 3	lautlt	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝐵 ) ) → ( 𝑋 ( lt ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ) )
34	26 27 28 32 33	syl13anc	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ) )
35		f1ocnvfv2	⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
36	30 35	sylancom	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
37	36	breq2d	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ↔ ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ) )
38	34 37	bitr2d	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ↔ 𝑋 ( lt ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑧 ) ) )
39		simplr3	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
40	1 4 3	lautlt	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ◡ 𝐹 ‘ 𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
41	26 27 32 39 40	syl13anc	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ◡ 𝐹 ‘ 𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
42	36	breq1d	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ↔ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
43	41 42	bitr2d	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ↔ ( ◡ 𝐹 ‘ 𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) )
44	38 43	anbi12d	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ↔ ( 𝑋 ( lt ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑧 ) ∧ ( ◡ 𝐹 ‘ 𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) ) )
45		breq2	⊢ ( 𝑤 = ( ◡ 𝐹 ‘ 𝑧 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ↔ 𝑋 ( lt ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑧 ) ) )
46		breq1	⊢ ( 𝑤 = ( ◡ 𝐹 ‘ 𝑧 ) → ( 𝑤 ( lt ‘ 𝐾 ) 𝑌 ↔ ( ◡ 𝐹 ‘ 𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) )
47	45 46	anbi12d	⊢ ( 𝑤 = ( ◡ 𝐹 ‘ 𝑧 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( 𝑋 ( lt ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑧 ) ∧ ( ◡ 𝐹 ‘ 𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) ) )
48	47	rspcev	⊢ ( ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝐵 ∧ ( 𝑋 ( lt ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑧 ) ∧ ( ◡ 𝐹 ‘ 𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) )
49	48	ex	⊢ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝐵 → ( ( 𝑋 ( lt ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑧 ) ∧ ( ◡ 𝐹 ‘ 𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑤 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) )
50	32 49	syl	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑧 ) ∧ ( ◡ 𝐹 ‘ 𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑤 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) )
51	44 50	sylbid	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) )
52	51	rexlimdva	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) )
53	25 52	impbid	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ∃ 𝑤 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) )
54	53	notbid	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ¬ ∃ 𝑤 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ¬ ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) )
55	5 54	anbi12d	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ∧ ¬ ∃ 𝑤 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) ) )
56	1 4 2	cvrval	⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ∧ ¬ ∃ 𝑤 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) ) )
57	56	3adant3r1	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ∧ ¬ ∃ 𝑤 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ∧ 𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) ) )
58		simpl	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐾 ∈ 𝐴 )
59		simpr1	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐹 ∈ 𝐼 )
60		simpr2	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
61	1 3	lautcl	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝐹 ∈ 𝐼 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
62	58 59 60 61	syl21anc	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
63		simpr3	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
64	1 3	lautcl	⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝐹 ∈ 𝐼 ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
65	58 59 63 64	syl21anc	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
66	1 4 2	cvrval	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) 𝐶 ( 𝐹 ‘ 𝑌 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) ) )
67	58 62 65 66	syl3anc	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) 𝐶 ( 𝐹 ‘ 𝑌 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ) ) )
68	55 57 67	3bitr4d	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) 𝐶 ( 𝐹 ‘ 𝑌 ) ) )