Metamath Proof Explorer

Theorem impprop

Description: The implication between two sentences of propositional calculus is a sentence of propositional calculus. (Contributed by Thomas van Maaren, 21-Aug-2026)

Ref Expression
Assertion impprop ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) → ( 𝑥 prop→ 𝑦 ) ∈ PROP )

Proof

Step Hyp Ref Expression
1 df-prop ⊢ PROP = setrecs ( ( 𝑤 ∈ V ↦ { 𝑧 ∣ ( ∃ 𝑣 ∈ 𝑤 ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } ) )
2 prex ⊢ { 𝑥 , 𝑦 } ∈ V
3 2 a1i ⊢ ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) → { 𝑥 , 𝑦 } ∈ V )
4 prssi ⊢ ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) → { 𝑥 , 𝑦 } ⊆ PROP )
5 1 3 4 setrec1 ⊢ ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) → ( ( 𝑤 ∈ V ↦ { 𝑧 ∣ ( ∃ 𝑣 ∈ 𝑤 ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } ) ‘ { 𝑥 , 𝑦 } ) ⊆ PROP )
6 vex ⊢ 𝑦 ∈ V
7 vex ⊢ 𝑥 ∈ V
8 oveq2 ⊢ ( 𝑣 = 𝑦 → ( 𝑢 prop→ 𝑣 ) = ( 𝑢 prop→ 𝑦 ) )
9 8 eqeq2d ⊢ ( 𝑣 = 𝑦 → ( 𝑧 = ( 𝑢 prop→ 𝑣 ) ↔ 𝑧 = ( 𝑢 prop→ 𝑦 ) ) )
10 oveq1 ⊢ ( 𝑢 = 𝑥 → ( 𝑢 prop→ 𝑦 ) = ( 𝑥 prop→ 𝑦 ) )
11 10 eqeq2d ⊢ ( 𝑢 = 𝑥 → ( 𝑧 = ( 𝑢 prop→ 𝑦 ) ↔ 𝑧 = ( 𝑥 prop→ 𝑦 ) ) )
12 6 7 9 11 ceqsex2v ⊢ ( ∃ 𝑣 ∃ 𝑢 ( 𝑣 = 𝑦 ∧ 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ↔ 𝑧 = ( 𝑥 prop→ 𝑦 ) )
13 12 bilanri ⊢ ( ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) ∧ 𝑧 = ( 𝑥 prop→ 𝑦 ) ) → ∃ 𝑣 ∃ 𝑢 ( 𝑣 = 𝑦 ∧ 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) )
14 3anass ⊢ ( ( 𝑣 = 𝑦 ∧ 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ↔ ( 𝑣 = 𝑦 ∧ ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
15 14 exbii ⊢ ( ∃ 𝑢 ( 𝑣 = 𝑦 ∧ 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ↔ ∃ 𝑢 ( 𝑣 = 𝑦 ∧ ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
16 19.42v ⊢ ( ∃ 𝑢 ( 𝑣 = 𝑦 ∧ ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) ↔ ( 𝑣 = 𝑦 ∧ ∃ 𝑢 ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
17 15 16 bitri ⊢ ( ∃ 𝑢 ( 𝑣 = 𝑦 ∧ 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ↔ ( 𝑣 = 𝑦 ∧ ∃ 𝑢 ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
18 17 exbii ⊢ ( ∃ 𝑣 ∃ 𝑢 ( 𝑣 = 𝑦 ∧ 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ↔ ∃ 𝑣 ( 𝑣 = 𝑦 ∧ ∃ 𝑢 ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
19 13 18 sylib ⊢ ( ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) ∧ 𝑧 = ( 𝑥 prop→ 𝑦 ) ) → ∃ 𝑣 ( 𝑣 = 𝑦 ∧ ∃ 𝑢 ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
20 olc ⊢ ( 𝑣 = 𝑦 → ( 𝑣 = 𝑥 ∨ 𝑣 = 𝑦 ) )
21 vex ⊢ 𝑣 ∈ V
22 21 elpr ⊢ ( 𝑣 ∈ { 𝑥 , 𝑦 } ↔ ( 𝑣 = 𝑥 ∨ 𝑣 = 𝑦 ) )
23 20 22 sylibr ⊢ ( 𝑣 = 𝑦 → 𝑣 ∈ { 𝑥 , 𝑦 } )
24 orc ⊢ ( 𝑢 = 𝑥 → ( 𝑢 = 𝑥 ∨ 𝑢 = 𝑦 ) )
25 vex ⊢ 𝑢 ∈ V
26 25 elpr ⊢ ( 𝑢 ∈ { 𝑥 , 𝑦 } ↔ ( 𝑢 = 𝑥 ∨ 𝑢 = 𝑦 ) )
27 24 26 sylibr ⊢ ( 𝑢 = 𝑥 → 𝑢 ∈ { 𝑥 , 𝑦 } )
28 27 anim1i ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) → ( 𝑢 ∈ { 𝑥 , 𝑦 } ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) )
29 28 eximi ⊢ ( ∃ 𝑢 ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) → ∃ 𝑢 ( 𝑢 ∈ { 𝑥 , 𝑦 } ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) )
30 df-rex ⊢ ( ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ↔ ∃ 𝑢 ( 𝑢 ∈ { 𝑥 , 𝑦 } ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) )
31 29 30 sylibr ⊢ ( ∃ 𝑢 ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) → ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) )
32 31 olcd ⊢ ( ∃ 𝑢 ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) → ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) )
33 23 32 anim12i ⊢ ( ( 𝑣 = 𝑦 ∧ ∃ 𝑢 ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) → ( 𝑣 ∈ { 𝑥 , 𝑦 } ∧ ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
34 33 eximi ⊢ ( ∃ 𝑣 ( 𝑣 = 𝑦 ∧ ∃ 𝑢 ( 𝑢 = 𝑥 ∧ 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) → ∃ 𝑣 ( 𝑣 ∈ { 𝑥 , 𝑦 } ∧ ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
35 19 34 syl ⊢ ( ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) ∧ 𝑧 = ( 𝑥 prop→ 𝑦 ) ) → ∃ 𝑣 ( 𝑣 ∈ { 𝑥 , 𝑦 } ∧ ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
36 df-rex ⊢ ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ↔ ∃ 𝑣 ( 𝑣 ∈ { 𝑥 , 𝑦 } ∧ ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
37 35 36 sylibr ⊢ ( ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) ∧ 𝑧 = ( 𝑥 prop→ 𝑦 ) ) → ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) )
38 37 orcd ⊢ ( ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) ∧ 𝑧 = ( 𝑥 prop→ 𝑦 ) ) → ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) )
39 38 ex ⊢ ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) → ( 𝑧 = ( 𝑥 prop→ 𝑦 ) → ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) ) )
40 39 alrimiv ⊢ ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) → ∀ 𝑧 ( 𝑧 = ( 𝑥 prop→ 𝑦 ) → ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) ) )
41 ovex ⊢ ( 𝑥 prop→ 𝑦 ) ∈ V
42 elab6g ⊢ ( ( 𝑥 prop→ 𝑦 ) ∈ V → ( ( 𝑥 prop→ 𝑦 ) ∈ { 𝑧 ∣ ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } ↔ ∀ 𝑧 ( 𝑧 = ( 𝑥 prop→ 𝑦 ) → ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) ) ) )
43 41 42 ax-mp ⊢ ( ( 𝑥 prop→ 𝑦 ) ∈ { 𝑧 ∣ ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } ↔ ∀ 𝑧 ( 𝑧 = ( 𝑥 prop→ 𝑦 ) → ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) ) )
44 40 43 sylibr ⊢ ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) → ( 𝑥 prop→ 𝑦 ) ∈ { 𝑧 ∣ ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } )
45 rexeq ⊢ ( 𝑤 = { 𝑥 , 𝑦 } → ( ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ↔ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) )
46 45 orbi2d ⊢ ( 𝑤 = { 𝑥 , 𝑦 } → ( ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ↔ ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
47 46 rexeqbi1dv ⊢ ( 𝑤 = { 𝑥 , 𝑦 } → ( ∃ 𝑣 ∈ 𝑤 ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ↔ ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ) )
48 47 orbi1d ⊢ ( 𝑤 = { 𝑥 , 𝑦 } → ( ( ∃ 𝑣 ∈ 𝑤 ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) ↔ ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) ) )
49 48 abbidv ⊢ ( 𝑤 = { 𝑥 , 𝑦 } → { 𝑧 ∣ ( ∃ 𝑣 ∈ 𝑤 ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } = { 𝑧 ∣ ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } )
50 eqid ⊢ ( 𝑤 ∈ V ↦ { 𝑧 ∣ ( ∃ 𝑣 ∈ 𝑤 ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } ) = ( 𝑤 ∈ V ↦ { 𝑧 ∣ ( ∃ 𝑣 ∈ 𝑤 ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } )
51 2 dfproplem ⊢ { 𝑧 ∣ ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } ∈ V
52 49 50 51 fvmpt ⊢ ( { 𝑥 , 𝑦 } ∈ V → ( ( 𝑤 ∈ V ↦ { 𝑧 ∣ ( ∃ 𝑣 ∈ 𝑤 ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } ) ‘ { 𝑥 , 𝑦 } ) = { 𝑧 ∣ ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } )
53 2 52 ax-mp ⊢ ( ( 𝑤 ∈ V ↦ { 𝑧 ∣ ( ∃ 𝑣 ∈ 𝑤 ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } ) ‘ { 𝑥 , 𝑦 } ) = { 𝑧 ∣ ( ∃ 𝑣 ∈ { 𝑥 , 𝑦 } ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ { 𝑥 , 𝑦 } 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) }
54 44 53 eleqtrrdi ⊢ ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) → ( 𝑥 prop→ 𝑦 ) ∈ ( ( 𝑤 ∈ V ↦ { 𝑧 ∣ ( ∃ 𝑣 ∈ 𝑤 ( 𝑧 = ( prop¬ ‘ 𝑣 ) ∨ ∃ 𝑢 ∈ 𝑤 𝑧 = ( 𝑢 prop→ 𝑣 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑧 = ( propvar ‘ 𝑛 ) ) } ) ‘ { 𝑥 , 𝑦 } ) )
55 5 54 sseldd ⊢ ( ( 𝑥 ∈ PROP ∧ 𝑦 ∈ PROP ) → ( 𝑥 prop→ 𝑦 ) ∈ PROP )