Metamath Proof Explorer


Theorem wemaplem3

Description: Lemma for wemapso . Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015) (Revised by AV, 21-Jul-2024)

Ref Expression
Hypotheses wemapso.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐴 ( ( 𝑥𝑧 ) 𝑆 ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
wemaplem2.p ( 𝜑𝑃 ∈ ( 𝐵m 𝐴 ) )
wemaplem2.x ( 𝜑𝑋 ∈ ( 𝐵m 𝐴 ) )
wemaplem2.q ( 𝜑𝑄 ∈ ( 𝐵m 𝐴 ) )
wemaplem2.r ( 𝜑𝑅 Or 𝐴 )
wemaplem2.s ( 𝜑𝑆 Po 𝐵 )
wemaplem3.px ( 𝜑𝑃 𝑇 𝑋 )
wemaplem3.xq ( 𝜑𝑋 𝑇 𝑄 )
Assertion wemaplem3 ( 𝜑𝑃 𝑇 𝑄 )

Proof

Step Hyp Ref Expression
1 wemapso.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐴 ( ( 𝑥𝑧 ) 𝑆 ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
2 wemaplem2.p ( 𝜑𝑃 ∈ ( 𝐵m 𝐴 ) )
3 wemaplem2.x ( 𝜑𝑋 ∈ ( 𝐵m 𝐴 ) )
4 wemaplem2.q ( 𝜑𝑄 ∈ ( 𝐵m 𝐴 ) )
5 wemaplem2.r ( 𝜑𝑅 Or 𝐴 )
6 wemaplem2.s ( 𝜑𝑆 Po 𝐵 )
7 wemaplem3.px ( 𝜑𝑃 𝑇 𝑋 )
8 wemaplem3.xq ( 𝜑𝑋 𝑇 𝑄 )
9 1 wemaplem1 ( ( 𝑃 ∈ ( 𝐵m 𝐴 ) ∧ 𝑋 ∈ ( 𝐵m 𝐴 ) ) → ( 𝑃 𝑇 𝑋 ↔ ∃ 𝑎𝐴 ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) )
10 2 3 9 syl2anc ( 𝜑 → ( 𝑃 𝑇 𝑋 ↔ ∃ 𝑎𝐴 ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) )
11 7 10 mpbid ( 𝜑 → ∃ 𝑎𝐴 ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) )
12 1 wemaplem1 ( ( 𝑋 ∈ ( 𝐵m 𝐴 ) ∧ 𝑄 ∈ ( 𝐵m 𝐴 ) ) → ( 𝑋 𝑇 𝑄 ↔ ∃ 𝑏𝐴 ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) )
13 3 4 12 syl2anc ( 𝜑 → ( 𝑋 𝑇 𝑄 ↔ ∃ 𝑏𝐴 ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) )
14 8 13 mpbid ( 𝜑 → ∃ 𝑏𝐴 ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) )
15 2 ad2antrr ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → 𝑃 ∈ ( 𝐵m 𝐴 ) )
16 3 ad2antrr ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → 𝑋 ∈ ( 𝐵m 𝐴 ) )
17 4 ad2antrr ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → 𝑄 ∈ ( 𝐵m 𝐴 ) )
18 5 ad2antrr ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → 𝑅 Or 𝐴 )
19 6 ad2antrr ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → 𝑆 Po 𝐵 )
20 simplrl ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → 𝑎𝐴 )
21 simp2rl ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) )
22 21 3expa ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) )
23 simprr ( ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) → ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) )
24 23 ad2antlr ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) )
25 simprl ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → 𝑏𝐴 )
26 simprrl ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) )
27 simprrr ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) )
28 1 15 16 17 18 19 20 22 24 25 26 27 wemaplem2 ( ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) ∧ ( 𝑏𝐴 ∧ ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) ) ) → 𝑃 𝑇 𝑄 )
29 28 rexlimdvaa ( ( 𝜑 ∧ ( 𝑎𝐴 ∧ ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) ) ) → ( ∃ 𝑏𝐴 ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) → 𝑃 𝑇 𝑄 ) )
30 29 rexlimdvaa ( 𝜑 → ( ∃ 𝑎𝐴 ( ( 𝑃𝑎 ) 𝑆 ( 𝑋𝑎 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃𝑐 ) = ( 𝑋𝑐 ) ) ) → ( ∃ 𝑏𝐴 ( ( 𝑋𝑏 ) 𝑆 ( 𝑄𝑏 ) ∧ ∀ 𝑐𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋𝑐 ) = ( 𝑄𝑐 ) ) ) → 𝑃 𝑇 𝑄 ) ) )
31 11 14 30 mp2d ( 𝜑𝑃 𝑇 𝑄 )