This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem glbconxN

Description: De Morgan's law for GLB and LUB. Index-set version of glbconN , where we read S as S ( i ) . (Contributed by NM, 17-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses glbcon.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
glbcon.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
glbcon.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
glbcon.o ⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion glbconxN ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) ) )

Proof

Step Hyp Ref Expression
1 glbcon.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 glbcon.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
3 glbcon.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
4 glbcon.o ⊢ ⊥ = ( oc ‘ 𝐾 )
5 vex ⊢ 𝑦 ∈ V
6 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑆 ↔ 𝑦 = 𝑆 ) )
7 6 rexbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 ↔ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 ) )
8 5 7 elab ⊢ ( 𝑦 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ↔ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 )
9 nfra1 ⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵
10 nfv ⊢ Ⅎ 𝑖 𝑦 ∈ 𝐵
11 rsp ⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( 𝑖 ∈ 𝐼 → 𝑆 ∈ 𝐵 ) )
12 eleq1a ⊢ ( 𝑆 ∈ 𝐵 → ( 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) )
13 11 12 syl6 ⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( 𝑖 ∈ 𝐼 → ( 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) ) )
14 9 10 13 rexlimd ⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) )
15 8 14 biimtrid ⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( 𝑦 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } → 𝑦 ∈ 𝐵 ) )
16 15 ssrdv ⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ⊆ 𝐵 )
17 1 2 3 4 glbconN ⊢ ( ( 𝐾 ∈ HL ∧ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ⊆ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) ) )
18 16 17 sylan2 ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) ) )
19 fvex ⊢ ( ⊥ ‘ 𝑦 ) ∈ V
20 eqeq1 ⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝑥 = 𝑆 ↔ ( ⊥ ‘ 𝑦 ) = 𝑆 ) )
21 20 rexbidv ⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 ↔ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) )
22 19 21 elab ⊢ ( ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ↔ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 )
23 22 rabbii ⊢ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } = { 𝑦 ∈ 𝐵 ∣ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 }
24 df-rab ⊢ { 𝑦 ∈ 𝐵 ∣ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) }
25 23 24 eqtri ⊢ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) }
26 nfv ⊢ Ⅎ 𝑖 𝐾 ∈ HL
27 26 9 nfan ⊢ Ⅎ 𝑖 ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 )
28 rspa ⊢ ( ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼 ) → 𝑆 ∈ 𝐵 )
29 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
30 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑆 ∈ 𝐵 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐵 )
31 29 30 sylan ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐵 )
32 eleq1a ⊢ ( ( ⊥ ‘ 𝑆 ) ∈ 𝐵 → ( 𝑦 = ( ⊥ ‘ 𝑆 ) → 𝑦 ∈ 𝐵 ) )
33 31 32 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) → 𝑦 ∈ 𝐵 ) )
34 33 pm4.71rd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 = ( ⊥ ‘ 𝑆 ) ) ) )
35 1 4 opcon2b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑆 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ 𝑦 = ( ⊥ ‘ 𝑆 ) ) )
36 29 35 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ 𝑦 = ( ⊥ ‘ 𝑆 ) ) )
37 36 3expa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ 𝑦 = ( ⊥ ‘ 𝑆 ) ) )
38 eqcom ⊢ ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ ( ⊥ ‘ 𝑦 ) = 𝑆 )
39 37 38 bitr3di ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( ⊥ ‘ 𝑦 ) = 𝑆 ) )
40 39 pm5.32da ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 = ( ⊥ ‘ 𝑆 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) )
41 34 40 bitrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) )
42 28 41 sylan2 ⊢ ( ( 𝐾 ∈ HL ∧ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼 ) ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) )
43 42 anassrs ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) )
44 27 43 rexbida ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ∃ 𝑖 ∈ 𝐼 ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) )
45 r19.42v ⊢ ( ∃ 𝑖 ∈ 𝐼 ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) )
46 44 45 bitr2di ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) ) )
47 46 abbidv ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) } = { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) } )
48 eqeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ 𝑥 = ( ⊥ ‘ 𝑆 ) ) )
49 48 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) ) )
50 49 cbvabv ⊢ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) }
51 47 50 eqtrdi ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } )
52 25 51 eqtrid ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } = { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } )
53 52 fveq2d ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) = ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) )
54 53 fveq2d ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) ) )
55 18 54 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) ) )