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

Metamath Proof Explorer

Theorem bnj1542

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1542.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
bnj1542.2 ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
bnj1542.3 ⊢ ( 𝜑 → 𝐹 ≠ 𝐺 )
bnj1542.4 ⊢ ( 𝑤 ∈ 𝐹 → ∀ 𝑥 𝑤 ∈ 𝐹 )
Assertion bnj1542 ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 bnj1542.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2 bnj1542.2 ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
3 bnj1542.3 ⊢ ( 𝜑 → 𝐹 ≠ 𝐺 )
4 bnj1542.4 ⊢ ( 𝑤 ∈ 𝐹 → ∀ 𝑥 𝑤 ∈ 𝐹 )
5 eqfnfv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) )
6 5 necon3abid ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 ≠ 𝐺 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) )
7 df-ne ⊢ ( ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ↔ ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
8 7 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
9 rexnal ⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
10 8 9 bitri ⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
11 6 10 bitr4di ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 ≠ 𝐺 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ) )
12 1 2 11 syl2anc ⊢ ( 𝜑 → ( 𝐹 ≠ 𝐺 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ) )
13 3 12 mpbid ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) )
14 nfv ⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 )
15 4 nfcii ⊢ Ⅎ 𝑥 𝐹
16 nfcv ⊢ Ⅎ 𝑥 𝑦
17 15 16 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
18 nfcv ⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑦 )
19 17 18 nfne ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 )
20 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
21 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) )
22 20 21 neeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ) )
23 14 19 22 cbvrexw ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) )
24 13 23 sylibr ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) )