MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iundom2g Structured version   Visualization version   GIF version

Theorem iundom2g 9309
Description: An upper bound for the cardinality of a disjoint indexed union, with explicit choice principles. 𝐵 depends on 𝑥 and should be thought of as 𝐵(𝑥). (Contributed by Mario Carneiro, 1-Sep-2015.)
Hypotheses
Ref Expression
iunfo.1 𝑇 = 𝑥𝐴 ({𝑥} × 𝐵)
iundomg.2 (𝜑 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴)
iundomg.3 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
Assertion
Ref Expression
iundom2g (𝜑𝑇 ≼ (𝐴 × 𝐶))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑇(𝑥)

Proof of Theorem iundom2g
Dummy variables 𝑓 𝑔 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iundomg.2 . . 3 (𝜑 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴)
2 iundomg.3 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
3 brdomi 7913 . . . . . . . . 9 (𝐵𝐶 → ∃𝑔 𝑔:𝐵1-1𝐶)
43adantl 482 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → ∃𝑔 𝑔:𝐵1-1𝐶)
5 f1f 6060 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐶𝑔:𝐵𝐶)
6 reldom 7908 . . . . . . . . . . . . . . 15 Rel ≼
76brrelex2i 5121 . . . . . . . . . . . . . 14 (𝐵𝐶𝐶 ∈ V)
86brrelexi 5120 . . . . . . . . . . . . . 14 (𝐵𝐶𝐵 ∈ V)
97, 8elmapd 7819 . . . . . . . . . . . . 13 (𝐵𝐶 → (𝑔 ∈ (𝐶𝑚 𝐵) ↔ 𝑔:𝐵𝐶))
109adantl 482 . . . . . . . . . . . 12 ((𝑥𝐴𝐵𝐶) → (𝑔 ∈ (𝐶𝑚 𝐵) ↔ 𝑔:𝐵𝐶))
115, 10syl5ibr 236 . . . . . . . . . . 11 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶𝑔 ∈ (𝐶𝑚 𝐵)))
12 ssiun2 4531 . . . . . . . . . . . . 13 (𝑥𝐴 → (𝐶𝑚 𝐵) ⊆ 𝑥𝐴 (𝐶𝑚 𝐵))
1312adantr 481 . . . . . . . . . . . 12 ((𝑥𝐴𝐵𝐶) → (𝐶𝑚 𝐵) ⊆ 𝑥𝐴 (𝐶𝑚 𝐵))
1413sseld 3583 . . . . . . . . . . 11 ((𝑥𝐴𝐵𝐶) → (𝑔 ∈ (𝐶𝑚 𝐵) → 𝑔 𝑥𝐴 (𝐶𝑚 𝐵)))
1511, 14syld 47 . . . . . . . . . 10 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶𝑔 𝑥𝐴 (𝐶𝑚 𝐵)))
1615ancrd 576 . . . . . . . . 9 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶 → (𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶)))
1716eximdv 1843 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → (∃𝑔 𝑔:𝐵1-1𝐶 → ∃𝑔(𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶)))
184, 17mpd 15 . . . . . . 7 ((𝑥𝐴𝐵𝐶) → ∃𝑔(𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶))
19 df-rex 2913 . . . . . . 7 (∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶 ↔ ∃𝑔(𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶))
2018, 19sylibr 224 . . . . . 6 ((𝑥𝐴𝐵𝐶) → ∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶)
2120ralimiaa 2946 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶)
222, 21syl 17 . . . 4 (𝜑 → ∀𝑥𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶)
23 nfv 1840 . . . . 5 𝑦𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶
24 nfiu1 4518 . . . . . 6 𝑥 𝑥𝐴 (𝐶𝑚 𝐵)
25 nfcv 2761 . . . . . . 7 𝑥𝑔
26 nfcsb1v 3531 . . . . . . 7 𝑥𝑦 / 𝑥𝐵
27 nfcv 2761 . . . . . . 7 𝑥𝐶
2825, 26, 27nff1 6058 . . . . . 6 𝑥 𝑔:𝑦 / 𝑥𝐵1-1𝐶
2924, 28nfrex 3001 . . . . 5 𝑥𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶
30 csbeq1a 3524 . . . . . . 7 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
31 f1eq2 6056 . . . . . . 7 (𝐵 = 𝑦 / 𝑥𝐵 → (𝑔:𝐵1-1𝐶𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3230, 31syl 17 . . . . . 6 (𝑥 = 𝑦 → (𝑔:𝐵1-1𝐶𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3332rexbidv 3045 . . . . 5 (𝑥 = 𝑦 → (∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶 ↔ ∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3423, 29, 33cbvral 3155 . . . 4 (∀𝑥𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶 ↔ ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶)
3522, 34sylib 208 . . 3 (𝜑 → ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶)
36 f1eq1 6055 . . . 4 (𝑔 = (𝑓𝑦) → (𝑔:𝑦 / 𝑥𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
3736acni3 8817 . . 3 (( 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴 ∧ ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶) → ∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
381, 35, 37syl2anc 692 . 2 (𝜑 → ∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
39 nfv 1840 . . . . . 6 𝑦(𝑓𝑥):𝐵1-1𝐶
40 nfcv 2761 . . . . . . 7 𝑥(𝑓𝑦)
4140, 26, 27nff1 6058 . . . . . 6 𝑥(𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶
42 fveq2 6150 . . . . . . . 8 (𝑥 = 𝑦 → (𝑓𝑥) = (𝑓𝑦))
43 f1eq1 6055 . . . . . . . 8 ((𝑓𝑥) = (𝑓𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝐵1-1𝐶))
4442, 43syl 17 . . . . . . 7 (𝑥 = 𝑦 → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝐵1-1𝐶))
45 f1eq2 6056 . . . . . . . 8 (𝐵 = 𝑦 / 𝑥𝐵 → ((𝑓𝑦):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4630, 45syl 17 . . . . . . 7 (𝑥 = 𝑦 → ((𝑓𝑦):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4744, 46bitrd 268 . . . . . 6 (𝑥 = 𝑦 → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4839, 41, 47cbvral 3155 . . . . 5 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ↔ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶)
49 df-ne 2791 . . . . . . . 8 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
50 acnrcl 8812 . . . . . . . . . 10 ( 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴𝐴 ∈ V)
511, 50syl 17 . . . . . . . . 9 (𝜑𝐴 ∈ V)
52 r19.2z 4034 . . . . . . . . . . . 12 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝐵𝐶) → ∃𝑥𝐴 𝐵𝐶)
537rexlimivw 3022 . . . . . . . . . . . 12 (∃𝑥𝐴 𝐵𝐶𝐶 ∈ V)
5452, 53syl 17 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝐵𝐶) → 𝐶 ∈ V)
5554expcom 451 . . . . . . . . . 10 (∀𝑥𝐴 𝐵𝐶 → (𝐴 ≠ ∅ → 𝐶 ∈ V))
562, 55syl 17 . . . . . . . . 9 (𝜑 → (𝐴 ≠ ∅ → 𝐶 ∈ V))
57 xpexg 6916 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 × 𝐶) ∈ V)
5851, 56, 57syl6an 567 . . . . . . . 8 (𝜑 → (𝐴 ≠ ∅ → (𝐴 × 𝐶) ∈ V))
5949, 58syl5bir 233 . . . . . . 7 (𝜑 → (¬ 𝐴 = ∅ → (𝐴 × 𝐶) ∈ V))
60 xpeq1 5090 . . . . . . . 8 (𝐴 = ∅ → (𝐴 × 𝐶) = (∅ × 𝐶))
61 0xp 5162 . . . . . . . . 9 (∅ × 𝐶) = ∅
62 0ex 4752 . . . . . . . . 9 ∅ ∈ V
6361, 62eqeltri 2694 . . . . . . . 8 (∅ × 𝐶) ∈ V
6460, 63syl6eqel 2706 . . . . . . 7 (𝐴 = ∅ → (𝐴 × 𝐶) ∈ V)
6559, 64pm2.61d2 172 . . . . . 6 (𝜑 → (𝐴 × 𝐶) ∈ V)
66 iunfo.1 . . . . . . . . . 10 𝑇 = 𝑥𝐴 ({𝑥} × 𝐵)
6766eleq2i 2690 . . . . . . . . 9 (𝑦𝑇𝑦 𝑥𝐴 ({𝑥} × 𝐵))
68 eliun 4492 . . . . . . . . 9 (𝑦 𝑥𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵))
6967, 68bitri 264 . . . . . . . 8 (𝑦𝑇 ↔ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵))
70 r19.29 3065 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)))
71 xp1st 7146 . . . . . . . . . . . . . . 15 (𝑦 ∈ ({𝑥} × 𝐵) → (1st𝑦) ∈ {𝑥})
7271ad2antll 764 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) ∈ {𝑥})
73 elsni 4167 . . . . . . . . . . . . . 14 ((1st𝑦) ∈ {𝑥} → (1st𝑦) = 𝑥)
7472, 73syl 17 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) = 𝑥)
75 simpl 473 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥𝐴)
7674, 75eqeltrd 2698 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) ∈ 𝐴)
7774fveq2d 6154 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓‘(1st𝑦)) = (𝑓𝑥))
7877fveq1d 6152 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓𝑥)‘(2nd𝑦)))
79 f1f 6060 . . . . . . . . . . . . . . 15 ((𝑓𝑥):𝐵1-1𝐶 → (𝑓𝑥):𝐵𝐶)
8079ad2antrl 763 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓𝑥):𝐵𝐶)
81 xp2nd 7147 . . . . . . . . . . . . . . 15 (𝑦 ∈ ({𝑥} × 𝐵) → (2nd𝑦) ∈ 𝐵)
8281ad2antll 764 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (2nd𝑦) ∈ 𝐵)
8380, 82ffvelrnd 6318 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓𝑥)‘(2nd𝑦)) ∈ 𝐶)
8478, 83eqeltrd 2698 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ 𝐶)
85 opelxpi 5110 . . . . . . . . . . . 12 (((1st𝑦) ∈ 𝐴 ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ 𝐶) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8676, 84, 85syl2anc 692 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8786rexlimiva 3021 . . . . . . . . . 10 (∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8870, 87syl 17 . . . . . . . . 9 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8988ex 450 . . . . . . . 8 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶)))
9069, 89syl5bi 232 . . . . . . 7 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑦𝑇 → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶)))
91 fvex 6160 . . . . . . . . . 10 (1st𝑦) ∈ V
92 fvex 6160 . . . . . . . . . 10 ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ V
9391, 92opth 4907 . . . . . . . . 9 (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ ((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))))
94 simpr 477 . . . . . . . . . . . . . . 15 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) = (1st𝑧))
9594fveq2d 6154 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (𝑓‘(1st𝑦)) = (𝑓‘(1st𝑧)))
9695fveq1d 6152 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → ((𝑓‘(1st𝑦))‘(2nd𝑧)) = ((𝑓‘(1st𝑧))‘(2nd𝑧)))
9796eqeq2d 2631 . . . . . . . . . . . 12 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))))
98 djussxp 5229 . . . . . . . . . . . . . . . . . 18 𝑥𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V)
9966, 98eqsstri 3616 . . . . . . . . . . . . . . . . 17 𝑇 ⊆ (𝐴 × V)
100 simprl 793 . . . . . . . . . . . . . . . . 17 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑦𝑇)
10199, 100sseldi 3582 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑦 ∈ (𝐴 × V))
102101adantr 481 . . . . . . . . . . . . . . 15 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → 𝑦 ∈ (𝐴 × V))
103 xp1st 7146 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐴 × V) → (1st𝑦) ∈ 𝐴)
104102, 103syl 17 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) ∈ 𝐴)
105 simpll 789 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → ∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶)
106 nfcv 2761 . . . . . . . . . . . . . . . 16 𝑥(𝑓‘(1st𝑦))
107 nfcsb1v 3531 . . . . . . . . . . . . . . . 16 𝑥(1st𝑦) / 𝑥𝐵
108106, 107, 27nff1 6058 . . . . . . . . . . . . . . 15 𝑥(𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶
109 fveq2 6150 . . . . . . . . . . . . . . . . 17 (𝑥 = (1st𝑦) → (𝑓𝑥) = (𝑓‘(1st𝑦)))
110 f1eq1 6055 . . . . . . . . . . . . . . . . 17 ((𝑓𝑥) = (𝑓‘(1st𝑦)) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):𝐵1-1𝐶))
111109, 110syl 17 . . . . . . . . . . . . . . . 16 (𝑥 = (1st𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):𝐵1-1𝐶))
112 csbeq1a 3524 . . . . . . . . . . . . . . . . 17 (𝑥 = (1st𝑦) → 𝐵 = (1st𝑦) / 𝑥𝐵)
113 f1eq2 6056 . . . . . . . . . . . . . . . . 17 (𝐵 = (1st𝑦) / 𝑥𝐵 → ((𝑓‘(1st𝑦)):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
114112, 113syl 17 . . . . . . . . . . . . . . . 16 (𝑥 = (1st𝑦) → ((𝑓‘(1st𝑦)):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
115111, 114bitrd 268 . . . . . . . . . . . . . . 15 (𝑥 = (1st𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
116108, 115rspc 3289 . . . . . . . . . . . . . 14 ((1st𝑦) ∈ 𝐴 → (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
117104, 105, 116sylc 65 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶)
118107nfel2 2777 . . . . . . . . . . . . . . . . . . . 20 𝑥(2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵
11974eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥 = (1st𝑦))
120119, 112syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝐵 = (1st𝑦) / 𝑥𝐵)
12182, 120eleqtrd 2700 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
122121ex 450 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐴 → (((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
123118, 122rexlimi 3017 . . . . . . . . . . . . . . . . . . 19 (∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
12470, 123syl 17 . . . . . . . . . . . . . . . . . 18 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
125124ex 450 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
12669, 125syl5bi 232 . . . . . . . . . . . . . . . 16 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑦𝑇 → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
127126imp 445 . . . . . . . . . . . . . . 15 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑦𝑇) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
128127adantrr 752 . . . . . . . . . . . . . 14 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
129128adantr 481 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
130126ralrimiv 2959 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ∀𝑦𝑇 (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
131 fveq2 6150 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (2nd𝑦) = (2nd𝑧))
132 fveq2 6150 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑧 → (1st𝑦) = (1st𝑧))
133132csbeq1d 3522 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧(1st𝑦) / 𝑥𝐵 = (1st𝑧) / 𝑥𝐵)
134131, 133eleq12d 2692 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵 ↔ (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵))
135134rspccva 3294 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝑇 (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵𝑧𝑇) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
136130, 135sylan 488 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑧𝑇) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
137136adantrl 751 . . . . . . . . . . . . . . 15 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
138137adantr 481 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
13994csbeq1d 3522 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) / 𝑥𝐵 = (1st𝑧) / 𝑥𝐵)
140138, 139eleqtrrd 2701 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑧) ∈ (1st𝑦) / 𝑥𝐵)
141 f1fveq 6476 . . . . . . . . . . . . 13 (((𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶 ∧ ((2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵 ∧ (2nd𝑧) ∈ (1st𝑦) / 𝑥𝐵)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
142117, 129, 140, 141syl12anc 1321 . . . . . . . . . . . 12 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
14397, 142bitr3d 270 . . . . . . . . . . 11 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
144143pm5.32da 672 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))) ↔ ((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧))))
145 simprr 795 . . . . . . . . . . . 12 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑧𝑇)
14699, 145sseldi 3582 . . . . . . . . . . 11 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑧 ∈ (𝐴 × V))
147 xpopth 7155 . . . . . . . . . . 11 ((𝑦 ∈ (𝐴 × V) ∧ 𝑧 ∈ (𝐴 × V)) → (((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧)) ↔ 𝑦 = 𝑧))
148101, 146, 147syl2anc 692 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧)) ↔ 𝑦 = 𝑧))
149144, 148bitrd 268 . . . . . . . . 9 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))) ↔ 𝑦 = 𝑧))
15093, 149syl5bb 272 . . . . . . . 8 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ 𝑦 = 𝑧))
151150ex 450 . . . . . . 7 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ((𝑦𝑇𝑧𝑇) → (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ 𝑦 = 𝑧)))
15290, 151dom2d 7943 . . . . . 6 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ((𝐴 × 𝐶) ∈ V → 𝑇 ≼ (𝐴 × 𝐶)))
15365, 152syl5com 31 . . . . 5 (𝜑 → (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑇 ≼ (𝐴 × 𝐶)))
15448, 153syl5bir 233 . . . 4 (𝜑 → (∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶𝑇 ≼ (𝐴 × 𝐶)))
155154adantld 483 . . 3 (𝜑 → ((𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶) → 𝑇 ≼ (𝐴 × 𝐶)))
156155exlimdv 1858 . 2 (𝜑 → (∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶) → 𝑇 ≼ (𝐴 × 𝐶)))
15738, 156mpd 15 1 (𝜑𝑇 ≼ (𝐴 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3186  csb 3515  wss 3556  c0 3893  {csn 4150  cop 4156   ciun 4487   class class class wbr 4615   × cxp 5074  wf 5845  1-1wf1 5846  cfv 5849  (class class class)co 6607  1st c1st 7114  2nd c2nd 7115  𝑚 cmap 7805  cdom 7900  AC wacn 8711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-1st 7116  df-2nd 7117  df-map 7807  df-dom 7904  df-acn 8715
This theorem is referenced by:  iundomg  9310  iundom  9311
  Copyright terms: Public domain W3C validator