Metamath Proof Explorer

Theorem fun11

Description: Two ways of stating that A is one-to-one (but not necessarily a function). Each side is equivalent to Definition 6.4(3) of TakeutiZaring p. 24, who use the notation "Un_2 (A)" for one-to-one (but not necessarily a function). (Contributed by NM, 17-Jan-2006)

Ref Expression
Assertion fun11 ( ( Fun ◡ ◡ 𝐴 ∧ Fun ◡ 𝐴 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 dfbi2 ⊢ ( ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑤 ) ↔ ( ( 𝑥 = 𝑧 → 𝑦 = 𝑤 ) ∧ ( 𝑦 = 𝑤 → 𝑥 = 𝑧 ) ) )
2 1 imbi2i ⊢ ( ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑤 ) ) ↔ ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( ( 𝑥 = 𝑧 → 𝑦 = 𝑤 ) ∧ ( 𝑦 = 𝑤 → 𝑥 = 𝑧 ) ) ) )
3 pm4.76 ⊢ ( ( ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 → 𝑦 = 𝑤 ) ) ∧ ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑦 = 𝑤 → 𝑥 = 𝑧 ) ) ) ↔ ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( ( 𝑥 = 𝑧 → 𝑦 = 𝑤 ) ∧ ( 𝑦 = 𝑤 → 𝑥 = 𝑧 ) ) ) )
4 bi2.04 ⊢ ( ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 → 𝑦 = 𝑤 ) ) ↔ ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) )
5 bi2.04 ⊢ ( ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑦 = 𝑤 → 𝑥 = 𝑧 ) ) ↔ ( 𝑦 = 𝑤 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) )
6 4 5 anbi12i ⊢ ( ( ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 → 𝑦 = 𝑤 ) ) ∧ ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑦 = 𝑤 → 𝑥 = 𝑧 ) ) ) ↔ ( ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) ∧ ( 𝑦 = 𝑤 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) ) )
7 2 3 6 3bitr2i ⊢ ( ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑤 ) ) ↔ ( ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) ∧ ( 𝑦 = 𝑤 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) ) )
8 7 2albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) ∧ ( 𝑦 = 𝑤 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) ) )
9 19.26-2 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) ∧ ( 𝑦 = 𝑤 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑤 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) ) )
10 alcom ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) )
11 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝐴 𝑦 ↔ 𝑧 𝐴 𝑦 ) )
12 11 anbi1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) ↔ ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) ) )
13 12 imbi1d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ↔ ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) )
14 13 equsalvw ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) ↔ ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) )
15 14 albii ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) ↔ ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) )
16 10 15 bitri ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) ↔ ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) )
17 breq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐴 𝑤 ) )
18 17 anbi1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) ↔ ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) ) )
19 18 imbi1d ⊢ ( 𝑦 = 𝑤 → ( ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ↔ ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) )
20 19 equsalvw ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑤 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) ↔ ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) )
21 20 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑤 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) ↔ ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) )
22 16 21 anbi12i ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑧 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑤 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) ) ↔ ( ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ∧ ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) )
23 8 9 22 3bitri ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ∧ ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) )
24 23 2albii ⊢ ( ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑧 ∀ 𝑤 ( ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ∧ ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) )
25 19.26-2 ⊢ ( ∀ 𝑧 ∀ 𝑤 ( ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ∧ ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) ↔ ( ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ∧ ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) )
26 24 25 bitr2i ⊢ ( ( ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ∧ ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑤 ) ) )
27 fun2cnv ⊢ ( Fun ◡ ◡ 𝐴 ↔ ∀ 𝑧 ∃* 𝑦 𝑧 𝐴 𝑦 )
28 breq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 𝐴 𝑦 ↔ 𝑧 𝐴 𝑤 ) )
29 28 mo4 ⊢ ( ∃* 𝑦 𝑧 𝐴 𝑦 ↔ ∀ 𝑦 ∀ 𝑤 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) )
30 29 albii ⊢ ( ∀ 𝑧 ∃* 𝑦 𝑧 𝐴 𝑦 ↔ ∀ 𝑧 ∀ 𝑦 ∀ 𝑤 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) )
31 alcom ⊢ ( ∀ 𝑦 ∀ 𝑤 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ↔ ∀ 𝑤 ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) )
32 31 albii ⊢ ( ∀ 𝑧 ∀ 𝑦 ∀ 𝑤 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) )
33 27 30 32 3bitri ⊢ ( Fun ◡ ◡ 𝐴 ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) )
34 funcnv2 ⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑤 ∃* 𝑥 𝑥 𝐴 𝑤 )
35 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝐴 𝑤 ↔ 𝑧 𝐴 𝑤 ) )
36 35 mo4 ⊢ ( ∃* 𝑥 𝑥 𝐴 𝑤 ↔ ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) )
37 36 albii ⊢ ( ∀ 𝑤 ∃* 𝑥 𝑥 𝐴 𝑤 ↔ ∀ 𝑤 ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) )
38 alcom ⊢ ( ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) )
39 38 albii ⊢ ( ∀ 𝑤 ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ↔ ∀ 𝑤 ∀ 𝑧 ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) )
40 alcom ⊢ ( ∀ 𝑤 ∀ 𝑧 ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) )
41 39 40 bitri ⊢ ( ∀ 𝑤 ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) )
42 34 37 41 3bitri ⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) )
43 33 42 anbi12i ⊢ ( ( Fun ◡ ◡ 𝐴 ∧ Fun ◡ 𝐴 ) ↔ ( ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( ( 𝑧 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → 𝑦 = 𝑤 ) ∧ ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ( ( 𝑥 𝐴 𝑤 ∧ 𝑧 𝐴 𝑤 ) → 𝑥 = 𝑧 ) ) )
44 alrot4 ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑤 ) ) )
45 26 43 44 3bitr4i ⊢ ( ( Fun ◡ ◡ 𝐴 ∧ Fun ◡ 𝐴 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐴 𝑤 ) → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑤 ) ) )