![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elixp2 | Structured version Visualization version GIF version |
Description: Membership in an infinite Cartesian product. See df-ixp 8794 for discussion of the notation. (Contributed by NM, 28-Sep-2006.) |
Ref | Expression |
---|---|
elixp2 | ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq1 6590 | . . . . 5 ⊢ (𝑓 = 𝐹 → (𝑓 Fn 𝐴 ↔ 𝐹 Fn 𝐴)) | |
2 | fveq1 6838 | . . . . . . 7 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥)) | |
3 | 2 | eleq1d 2822 | . . . . . 6 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑥) ∈ 𝐵 ↔ (𝐹‘𝑥) ∈ 𝐵)) |
4 | 3 | ralbidv 3172 | . . . . 5 ⊢ (𝑓 = 𝐹 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
5 | 1, 4 | anbi12d 631 | . . . 4 ⊢ (𝑓 = 𝐹 → ((𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))) |
6 | dfixp 8795 | . . . 4 ⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} | |
7 | 5, 6 | elab2g 3630 | . . 3 ⊢ (𝐹 ∈ V → (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))) |
8 | 7 | pm5.32i 575 | . 2 ⊢ ((𝐹 ∈ V ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))) |
9 | elex 3461 | . . 3 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 ∈ V) | |
10 | 9 | pm4.71ri 561 | . 2 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐵)) |
11 | 3anass 1095 | . 2 ⊢ ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))) | |
12 | 8, 10, 11 | 3bitr4i 302 | 1 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3062 Vcvv 3443 Fn wfn 6488 ‘cfv 6493 Xcixp 8793 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3063 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-iota 6445 df-fun 6495 df-fn 6496 df-fv 6501 df-ixp 8794 |
This theorem is referenced by: fvixp 8798 ixpfn 8799 elixp 8800 ixpf 8816 resixp 8829 undifixp 8830 mptelixpg 8831 prdsbasprj 17314 xpsfrnel 17404 xpscf 17407 isssc 17663 isfuncd 17711 funcres2b 17743 dprdw 19748 ptrecube 36016 kelac1 41299 elixpconstg 43210 fvixp2 43324 rrxsnicc 44442 ioorrnopnxrlem 44448 hoiqssbllem1 44764 iinhoiicclem 44815 iunhoiioolem 44817 funcf2lem 46939 |
Copyright terms: Public domain | W3C validator |