Step | Hyp | Ref
| Expression |
1 | | iundomg.2 |
. . 3
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) ∈ AC 𝐴) |
2 | | iundomg.3 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ≼ 𝐶) |
3 | | brdomi 8662 |
. . . . . . . . 9
⊢ (𝐵 ≼ 𝐶 → ∃𝑔 𝑔:𝐵–1-1→𝐶) |
4 | 3 | adantl 485 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → ∃𝑔 𝑔:𝐵–1-1→𝐶) |
5 | | f1f 6636 |
. . . . . . . . . . . 12
⊢ (𝑔:𝐵–1-1→𝐶 → 𝑔:𝐵⟶𝐶) |
6 | | reldom 8655 |
. . . . . . . . . . . . . . 15
⊢ Rel
≼ |
7 | 6 | brrelex2i 5623 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ≼ 𝐶 → 𝐶 ∈ V) |
8 | 6 | brrelex1i 5622 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ≼ 𝐶 → 𝐵 ∈ V) |
9 | 7, 8 | elmapd 8545 |
. . . . . . . . . . . . 13
⊢ (𝐵 ≼ 𝐶 → (𝑔 ∈ (𝐶 ↑m 𝐵) ↔ 𝑔:𝐵⟶𝐶)) |
10 | 9 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝑔 ∈ (𝐶 ↑m 𝐵) ↔ 𝑔:𝐵⟶𝐶)) |
11 | 5, 10 | syl5ibr 249 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝑔:𝐵–1-1→𝐶 → 𝑔 ∈ (𝐶 ↑m 𝐵))) |
12 | | ssiun2 4972 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → (𝐶 ↑m 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)) |
13 | 12 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝐶 ↑m 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)) |
14 | 13 | sseld 3916 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝑔 ∈ (𝐶 ↑m 𝐵) → 𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵))) |
15 | 11, 14 | syld 47 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝑔:𝐵–1-1→𝐶 → 𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵))) |
16 | 15 | ancrd 555 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝑔:𝐵–1-1→𝐶 → (𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) ∧ 𝑔:𝐵–1-1→𝐶))) |
17 | 16 | eximdv 1925 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (∃𝑔 𝑔:𝐵–1-1→𝐶 → ∃𝑔(𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) ∧ 𝑔:𝐵–1-1→𝐶))) |
18 | 4, 17 | mpd 15 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → ∃𝑔(𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) ∧ 𝑔:𝐵–1-1→𝐶)) |
19 | | df-rex 3069 |
. . . . . . 7
⊢
(∃𝑔 ∈
∪ 𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:𝐵–1-1→𝐶 ↔ ∃𝑔(𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) ∧ 𝑔:𝐵–1-1→𝐶)) |
20 | 18, 19 | sylibr 237 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:𝐵–1-1→𝐶) |
21 | 20 | ralimiaa 3085 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ≼ 𝐶 → ∀𝑥 ∈ 𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:𝐵–1-1→𝐶) |
22 | 2, 21 | syl 17 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:𝐵–1-1→𝐶) |
23 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑦∃𝑔 ∈ ∪ 𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:𝐵–1-1→𝐶 |
24 | | nfiu1 4954 |
. . . . . 6
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) |
25 | | nfcv 2906 |
. . . . . . 7
⊢
Ⅎ𝑥𝑔 |
26 | | nfcsb1v 3852 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
27 | | nfcv 2906 |
. . . . . . 7
⊢
Ⅎ𝑥𝐶 |
28 | 25, 26, 27 | nff1 6634 |
. . . . . 6
⊢
Ⅎ𝑥 𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶 |
29 | 24, 28 | nfrex 3237 |
. . . . 5
⊢
Ⅎ𝑥∃𝑔 ∈ ∪ 𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶 |
30 | | csbeq1a 3841 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
31 | | f1eq2 6632 |
. . . . . . 7
⊢ (𝐵 = ⦋𝑦 / 𝑥⦌𝐵 → (𝑔:𝐵–1-1→𝐶 ↔ 𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑔:𝐵–1-1→𝐶 ↔ 𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
33 | 32 | rexbidv 3225 |
. . . . 5
⊢ (𝑥 = 𝑦 → (∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:𝐵–1-1→𝐶 ↔ ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
34 | 23, 29, 33 | cbvralw 3363 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:𝐵–1-1→𝐶 ↔ ∀𝑦 ∈ 𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) |
35 | 22, 34 | sylib 221 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) |
36 | | f1eq1 6631 |
. . . 4
⊢ (𝑔 = (𝑓‘𝑦) → (𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
37 | 36 | acni3 9688 |
. . 3
⊢
((∪ 𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) ∈ AC 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵)𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) → ∃𝑓(𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
38 | 1, 35, 37 | syl2anc 587 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
39 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑦(𝑓‘𝑥):𝐵–1-1→𝐶 |
40 | | nfcv 2906 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑓‘𝑦) |
41 | 40, 26, 27 | nff1 6634 |
. . . . . 6
⊢
Ⅎ𝑥(𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶 |
42 | | fveq2 6738 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑓‘𝑥) = (𝑓‘𝑦)) |
43 | | f1eq1 6631 |
. . . . . . . 8
⊢ ((𝑓‘𝑥) = (𝑓‘𝑦) → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):𝐵–1-1→𝐶)) |
44 | 42, 43 | syl 17 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):𝐵–1-1→𝐶)) |
45 | | f1eq2 6632 |
. . . . . . . 8
⊢ (𝐵 = ⦋𝑦 / 𝑥⦌𝐵 → ((𝑓‘𝑦):𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
46 | 30, 45 | syl 17 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑓‘𝑦):𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
47 | 44, 46 | bitrd 282 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
48 | 39, 41, 47 | cbvralw 3363 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ↔ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) |
49 | | df-ne 2943 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
50 | | acnrcl 9683 |
. . . . . . . . . 10
⊢ (∪ 𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) ∈ AC 𝐴 → 𝐴 ∈ V) |
51 | 1, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ V) |
52 | | r19.2z 4422 |
. . . . . . . . . . . 12
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ≼ 𝐶) → ∃𝑥 ∈ 𝐴 𝐵 ≼ 𝐶) |
53 | 7 | rexlimivw 3210 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝐴 𝐵 ≼ 𝐶 → 𝐶 ∈ V) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ≼ 𝐶) → 𝐶 ∈ V) |
55 | 54 | expcom 417 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 𝐵 ≼ 𝐶 → (𝐴 ≠ ∅ → 𝐶 ∈ V)) |
56 | 2, 55 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ≠ ∅ → 𝐶 ∈ V)) |
57 | | xpexg 7556 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 × 𝐶) ∈ V) |
58 | 51, 56, 57 | syl6an 684 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ≠ ∅ → (𝐴 × 𝐶) ∈ V)) |
59 | 49, 58 | syl5bir 246 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝐴 = ∅ → (𝐴 × 𝐶) ∈ V)) |
60 | | xpeq1 5582 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (𝐴 × 𝐶) = (∅ × 𝐶)) |
61 | | 0xp 5663 |
. . . . . . . . 9
⊢ (∅
× 𝐶) =
∅ |
62 | | 0ex 5216 |
. . . . . . . . 9
⊢ ∅
∈ V |
63 | 61, 62 | eqeltri 2836 |
. . . . . . . 8
⊢ (∅
× 𝐶) ∈
V |
64 | 60, 63 | eqeltrdi 2848 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝐴 × 𝐶) ∈ V) |
65 | 59, 64 | pm2.61d2 184 |
. . . . . 6
⊢ (𝜑 → (𝐴 × 𝐶) ∈ V) |
66 | | iunfo.1 |
. . . . . . . . . 10
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
67 | 66 | eleq2i 2831 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑇 ↔ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
68 | | eliun 4924 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵)) |
69 | 67, 68 | bitri 278 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑇 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵)) |
70 | | r19.29 3183 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ∃𝑥 ∈ 𝐴 ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) |
71 | | xp1st 7814 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ({𝑥} × 𝐵) → (1st ‘𝑦) ∈ {𝑥}) |
72 | 71 | ad2antll 729 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (1st ‘𝑦) ∈ {𝑥}) |
73 | | elsni 4574 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑦) ∈ {𝑥} → (1st ‘𝑦) = 𝑥) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (1st ‘𝑦) = 𝑥) |
75 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥 ∈ 𝐴) |
76 | 74, 75 | eqeltrd 2840 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (1st ‘𝑦) ∈ 𝐴) |
77 | 74 | fveq2d 6742 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓‘(1st ‘𝑦)) = (𝑓‘𝑥)) |
78 | 77 | fveq1d 6740 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘𝑥)‘(2nd ‘𝑦))) |
79 | | f1f 6636 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑥):𝐵–1-1→𝐶 → (𝑓‘𝑥):𝐵⟶𝐶) |
80 | 79 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓‘𝑥):𝐵⟶𝐶) |
81 | | xp2nd 7815 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑦) ∈ 𝐵) |
82 | 81 | ad2antll 729 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (2nd ‘𝑦) ∈ 𝐵) |
83 | 80, 82 | ffvelrnd 6926 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘𝑥)‘(2nd ‘𝑦)) ∈ 𝐶) |
84 | 78, 83 | eqeltrd 2840 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) ∈ 𝐶) |
85 | 76, 84 | opelxpd 5606 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → 〈(1st
‘𝑦), ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑦))〉 ∈ (𝐴 × 𝐶)) |
86 | 85 | rexlimiva 3209 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝐴 ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵)) → 〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 ∈
(𝐴 × 𝐶)) |
87 | 70, 86 | syl 17 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → 〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 ∈
(𝐴 × 𝐶)) |
88 | 87 | ex 416 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → (∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵) → 〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 ∈
(𝐴 × 𝐶))) |
89 | 69, 88 | syl5bi 245 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → (𝑦 ∈ 𝑇 → 〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 ∈
(𝐴 × 𝐶))) |
90 | | fvex 6751 |
. . . . . . . . . 10
⊢
(1st ‘𝑦) ∈ V |
91 | | fvex 6751 |
. . . . . . . . . 10
⊢ ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑦)) ∈ V |
92 | 90, 91 | opth 5376 |
. . . . . . . . 9
⊢
(〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 =
〈(1st ‘𝑧), ((𝑓‘(1st ‘𝑧))‘(2nd
‘𝑧))〉 ↔
((1st ‘𝑦)
= (1st ‘𝑧)
∧ ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧)))) |
93 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (1st
‘𝑦) = (1st
‘𝑧)) |
94 | 93 | fveq2d 6742 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (𝑓‘(1st ‘𝑦)) = (𝑓‘(1st ‘𝑧))) |
95 | 94 | fveq1d 6740 |
. . . . . . . . . . . . 13
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑧)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧))) |
96 | 95 | eqeq2d 2750 |
. . . . . . . . . . . 12
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑧)) ↔ ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧)))) |
97 | | djussxp 5731 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V) |
98 | 66, 97 | eqsstri 3951 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑇 ⊆ (𝐴 × V) |
99 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑦 ∈ 𝑇) |
100 | 98, 99 | sselid 3914 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑦 ∈ (𝐴 × V)) |
101 | 100 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → 𝑦 ∈ (𝐴 × V)) |
102 | | xp1st 7814 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝐴 × V) → (1st
‘𝑦) ∈ 𝐴) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (1st
‘𝑦) ∈ 𝐴) |
104 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶) |
105 | | nfcv 2906 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑓‘(1st ‘𝑦)) |
106 | | nfcsb1v 3852 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋(1st ‘𝑦) / 𝑥⦌𝐵 |
107 | 105, 106,
27 | nff1 6634 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑓‘(1st
‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶 |
108 | | fveq2 6738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (1st ‘𝑦) → (𝑓‘𝑥) = (𝑓‘(1st ‘𝑦))) |
109 | | f1eq1 6631 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑥) = (𝑓‘(1st ‘𝑦)) → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘(1st ‘𝑦)):𝐵–1-1→𝐶)) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (1st ‘𝑦) → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘(1st ‘𝑦)):𝐵–1-1→𝐶)) |
111 | | csbeq1a 3841 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (1st ‘𝑦) → 𝐵 = ⦋(1st
‘𝑦) / 𝑥⦌𝐵) |
112 | | f1eq2 6632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 =
⦋(1st ‘𝑦) / 𝑥⦌𝐵 → ((𝑓‘(1st ‘𝑦)):𝐵–1-1→𝐶 ↔ (𝑓‘(1st ‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶)) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (1st ‘𝑦) → ((𝑓‘(1st ‘𝑦)):𝐵–1-1→𝐶 ↔ (𝑓‘(1st ‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶)) |
114 | 110, 113 | bitrd 282 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (1st ‘𝑦) → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘(1st ‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶)) |
115 | 107, 114 | rspc 3539 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑦) ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → (𝑓‘(1st ‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶)) |
116 | 103, 104,
115 | sylc 65 |
. . . . . . . . . . . . 13
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (𝑓‘(1st ‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶) |
117 | 106 | nfel2 2924 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(2nd ‘𝑦) ∈ ⦋(1st
‘𝑦) / 𝑥⦌𝐵 |
118 | 74 | eqcomd 2745 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥 = (1st ‘𝑦)) |
119 | 118, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → 𝐵 = ⦋(1st
‘𝑦) / 𝑥⦌𝐵) |
120 | 82, 119 | eleqtrd 2842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
121 | 120 | ex 416 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐴 → (((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵)) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵)) |
122 | 117, 121 | rexlimi 3243 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑥 ∈
𝐴 ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵)) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
123 | 70, 122 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
124 | 123 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → (∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵)) |
125 | 69, 124 | syl5bi 245 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → (𝑦 ∈ 𝑇 → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵)) |
126 | 125 | imp 410 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ 𝑇) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
127 | 126 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
128 | 127 | adantr 484 |
. . . . . . . . . . . . 13
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (2nd
‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
129 | 125 | ralrimiv 3106 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → ∀𝑦 ∈ 𝑇 (2nd ‘𝑦) ∈ ⦋(1st
‘𝑦) / 𝑥⦌𝐵) |
130 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → (2nd ‘𝑦) = (2nd ‘𝑧)) |
131 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑧 → (1st ‘𝑦) = (1st ‘𝑧)) |
132 | 131 | csbeq1d 3831 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → ⦋(1st
‘𝑦) / 𝑥⦌𝐵 = ⦋(1st
‘𝑧) / 𝑥⦌𝐵) |
133 | 130, 132 | eleq12d 2834 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑧 → ((2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵 ↔ (2nd ‘𝑧) ∈
⦋(1st ‘𝑧) / 𝑥⦌𝐵)) |
134 | 133 | rspccva 3550 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑦 ∈
𝑇 (2nd
‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵 ∧ 𝑧 ∈ 𝑇) → (2nd ‘𝑧) ∈
⦋(1st ‘𝑧) / 𝑥⦌𝐵) |
135 | 129, 134 | sylan 583 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑧 ∈ 𝑇) → (2nd ‘𝑧) ∈
⦋(1st ‘𝑧) / 𝑥⦌𝐵) |
136 | 135 | adantrl 716 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (2nd ‘𝑧) ∈
⦋(1st ‘𝑧) / 𝑥⦌𝐵) |
137 | 136 | adantr 484 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (2nd
‘𝑧) ∈
⦋(1st ‘𝑧) / 𝑥⦌𝐵) |
138 | 93 | csbeq1d 3831 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) →
⦋(1st ‘𝑦) / 𝑥⦌𝐵 = ⦋(1st
‘𝑧) / 𝑥⦌𝐵) |
139 | 137, 138 | eleqtrrd 2843 |
. . . . . . . . . . . . 13
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (2nd
‘𝑧) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
140 | | f1fveq 7095 |
. . . . . . . . . . . . 13
⊢ (((𝑓‘(1st
‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶 ∧ ((2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵 ∧ (2nd ‘𝑧) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵)) → (((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑧)) ↔ (2nd
‘𝑦) = (2nd
‘𝑧))) |
141 | 116, 128,
139, 140 | syl12anc 837 |
. . . . . . . . . . . 12
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑧)) ↔ (2nd
‘𝑦) = (2nd
‘𝑧))) |
142 | 96, 141 | bitr3d 284 |
. . . . . . . . . . 11
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧)) ↔ (2nd
‘𝑦) = (2nd
‘𝑧))) |
143 | 142 | pm5.32da 582 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((1st ‘𝑦) = (1st ‘𝑧) ∧ ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧))) ↔ ((1st
‘𝑦) = (1st
‘𝑧) ∧
(2nd ‘𝑦) =
(2nd ‘𝑧)))) |
144 | | simprr 773 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑧 ∈ 𝑇) |
145 | 98, 144 | sselid 3914 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑧 ∈ (𝐴 × V)) |
146 | | xpopth 7823 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (𝐴 × V) ∧ 𝑧 ∈ (𝐴 × V)) → (((1st
‘𝑦) = (1st
‘𝑧) ∧
(2nd ‘𝑦) =
(2nd ‘𝑧))
↔ 𝑦 = 𝑧)) |
147 | 100, 145,
146 | syl2anc 587 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((1st ‘𝑦) = (1st ‘𝑧) ∧ (2nd
‘𝑦) = (2nd
‘𝑧)) ↔ 𝑦 = 𝑧)) |
148 | 143, 147 | bitrd 282 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((1st ‘𝑦) = (1st ‘𝑧) ∧ ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧))) ↔ 𝑦 = 𝑧)) |
149 | 92, 148 | syl5bb 286 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (〈(1st
‘𝑦), ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑦))〉 = 〈(1st
‘𝑧), ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧))〉 ↔ 𝑦 = 𝑧)) |
150 | 149 | ex 416 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → ((𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → (〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 =
〈(1st ‘𝑧), ((𝑓‘(1st ‘𝑧))‘(2nd
‘𝑧))〉 ↔
𝑦 = 𝑧))) |
151 | 89, 150 | dom2d 8694 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → ((𝐴 × 𝐶) ∈ V → 𝑇 ≼ (𝐴 × 𝐶))) |
152 | 65, 151 | syl5com 31 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → 𝑇 ≼ (𝐴 × 𝐶))) |
153 | 48, 152 | syl5bir 246 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶 → 𝑇 ≼ (𝐴 × 𝐶))) |
154 | 153 | adantld 494 |
. . 3
⊢ (𝜑 → ((𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) → 𝑇 ≼ (𝐴 × 𝐶))) |
155 | 154 | exlimdv 1941 |
. 2
⊢ (𝜑 → (∃𝑓(𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 (𝐶 ↑m 𝐵) ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) → 𝑇 ≼ (𝐴 × 𝐶))) |
156 | 38, 155 | mpd 15 |
1
⊢ (𝜑 → 𝑇 ≼ (𝐴 × 𝐶)) |